induction_top — Mathlib

English

Let α be a linear order with a bottom element ⊥. Then max ⊥ a = a for all a ∈ α.

Русский

Пусть α имеет нижнюю границу ⊥. Тогда max ⊥ a = a для любого a.

LaTeX

$$$\\max(\\bot, a) = a$$$

Lean4

@[elab_as_elim]
theorem induction_top [Preorder α] [WellFoundedGT α] [OrderTop α] {P : α → Prop} (hexists : ∃ M, P M)
    (hind : ∀ N ≠ ⊤, P N → ∃ M > N, P M) : P ⊤ := by
  contrapose! hexists
  intro M
  induction M using WellFoundedGT.induction with
  | ind x IH =>
    by_cases hx : x = ⊤
    · exact hx ▸ hexists
    · intro hx'
      obtain ⟨M, hM, hM'⟩ := hind x hx hx'
      exact IH _ hM hM'

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