【Lean4】ext

ext

関数や構造が等しいことを、各要素での等しさに帰着させる

Plaintext

example (f g : α → β)
    (h : ∀ x, f x = g x) :
    f = g := by
  funext x
  exact h x

example :
    myFrobenius K p = frobenius K p := by
  ext x
  rfl

example (f g : α → β)
    (h : ∀ x, f x = g x) :
    f = g := by
  funext x
  exact h x

example :
    myFrobenius K p = frobenius K p := by
  ext x
  rfl

Lean4の関連記事

【Lean4】namespace
【Lean4】section
【Lean4】variable
【Lean4】abbrev
【Lean4】constructor
【Lean4】#check
【Lean4】def
【Lean4】exact
【Lean4】rfl
【Lean4】intro
【Lean4】apply
【Lean4】unfold
【Lean4】rw
【Lean4】simp
【Lean4】simpa
【Lean4】constructor
【Lean4】left,right
【Lean4】cases
【Lean4】rcases
【Lean4】refine
【Lean4】use
【Lean4】have
【Lean4】show
【Lean4】change
【Lean4】subst
【Lean4】by_cases
【Lean4】induction
【Lean4】ext
【Lean4】funext
【Lean4】congrArg
【Lean4】norm_num
【Lean4】ring
【Lean4】linarith
【Lean4】aesop
【Lean4】structure
【Lean4】where
【Lean4】@[simp]
【Lean4】 #eval
【Lean4】let
【Lean4】if（条件分岐）
【Lean4】match（パターンマッチ）
【Lean4】リスト
【Lean4】Option
【Lean4】inductive