eq_top_iff_forall_ge — Mathlib

English

For x ∈ WithBot (WithTop α), x = ⊤ if and only if ∀ a ∈ α, a ≤ x.

Русский

Для x ∈ WithBot (WithTop α) верно: x = ⊤ тогда и только тогда, когда ∀ a ∈ α, a ≤ x.

LaTeX

$$$x = \\top \\iff \\forall a:\\alpha, a \\le x$$$

Lean4

theorem eq_top_iff_forall_ge [Preorder α] [Nonempty α] [NoTopOrder α] {x : WithBot (WithTop α)} :
    x = ⊤ ↔ ∀ a : α, a ≤ x := by
  refine ⟨by simp_all, fun H ↦ ?_⟩
  induction x
  · simp at H
  · simpa [WithTop.eq_top_iff_forall_ge] using H

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