eq_bot_iff_forall_le — Mathlib

English

Let x ∈ WithBot α and assume NoBotOrder α. Then x = ⊥ if and only if ∀ b : α, x ≤ b.

Русский

Пусть x ∈ WithBot α и предполагается NoBotOrder α. Тогда x = ⊥ тогда и только тогда, когда для всех b ∈ α выполняется x ≤ b.

LaTeX

$$$x = \bot \iff ∀ b : \alpha, x \le b$$$

Lean4

theorem eq_bot_iff_forall_le [NoBotOrder α] : x = ⊥ ↔ ∀ b : α, x ≤ b :=
  by
  refine ⟨by simp +contextual, fun h ↦ (x.eq_bot_iff_forall_ne).2 fun y => ?_⟩
  rintro rfl
  exact not_isBot y fun z => coe_le_coe.1 (h z)

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