isAtom_iff_le_of_ge — Mathlib

English

An element a is an atom iff a ≠ ⊥ and every non-bottom b ≤ a satisfies a ≤ b.

Русский

Элемент a является атомом тогда и только тогда, когда a ≠ ⊥ и каждый ненулевой b ≤ a удовлетворяет a ≤ b.

LaTeX

$$$IsAtom(a) \\iff a \\neq \\bot \\land \\forall b \\neq \\bot,\\ (b \\le a) \\rightarrow (a \\le b).$$$

Lean4

theorem isAtom_iff_le_of_ge : IsAtom a ↔ a ≠ ⊥ ∧ ∀ b ≠ ⊥, b ≤ a → a ≤ b :=
  and_congr Iff.rfl <|
    forall_congr' fun b => by simp only [Ne, @not_imp_comm (b = ⊥), Classical.not_imp, lt_iff_le_not_ge]

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