ext — Mathlib

English

Let f,g be normal functions. Then f = g if and only if f(⊥) = g(⊥) and for all a, f(a) = g(a) implies f(succ a) = g(succ a).

Русский

Пусть f и g — нормальные отображения. Тогда f = g тогда и только тогда, когда f(⊥) = g(⊥) и для всех a выполняется f(a) = g(a) ⇒ f( successor(a) ) = g( successor(a) ).

LaTeX

$$$\\forall \\{f,g : α \\to β\\}, \\mathrm{IsNormal}(f) \\land \\mathrm{IsNormal}(g) \\rightarrow \\left( f = g \\iff f(\\bot) = g(\\bot) \\wedge \\forall a, f(a) = g(a) \\rightarrow f(\\mathrm{succ}(a)) = g(\\mathrm{succ}(a)) \\right).$$

Lean4

protected theorem ext [OrderBot α] {g : α → β} (hf : IsNormal f) (hg : IsNormal g) :
    f = g ↔ f ⊥ = g ⊥ ∧ ∀ a, f a = g a → f (succ a) = g (succ a) :=
  by
  constructor
  · simp_all
  rintro ⟨H₁, H₂⟩
  ext a
  induction a using SuccOrder.limitRecOn with
  | isMin a ha => rw [ha.eq_bot, H₁]
  | succ a ha IH => exact H₂ a IH
  | isSuccLimit a ha IH =>
    apply (hf.isLUB_image_Iio_of_isSuccLimit ha).unique
    convert hg.isLUB_image_Iio_of_isSuccLimit ha using 1
    aesop

Похожие утверждения