【Lean4】funext

funext

関数の等しさを、すべての入力での値の等しさに変える

Plaintext

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

/-
目標が、
⊢ f = g
から、
x : α
⊢ f x = g x
になる
-/

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

/-
目標が、
⊢ f = g
から、
x : α
⊢ f x = g x
になる
-/