English
In a Boolean algebra that is atomic, x ≤ y iff for every atom a, a ≤ x implies a ≤ y.
Русский
В булевой алгебре, атомарной, выполняется: x ≤ y тогда и только тогда, когда для каждого атома a верно: a ≤ x ⇒ a ≤ y.
LaTeX
$$$ x \\le y \\iff \\forall a, IsAtom a \\rightarrow a \\le x \\rightarrow a \\le y $$$
Lean4
theorem le_iff_atom_le_imp {α} [BooleanAlgebra α] [IsAtomic α] {x y : α} : x ≤ y ↔ ∀ a, IsAtom a → a ≤ x → a ≤ y :=
by
refine ⟨fun h a _ => (le_trans · h), fun h => ?_⟩
have : x ⊓ yᶜ = ⊥ :=
of_not_not fun hbot =>
have ⟨a, ha, hle⟩ := (eq_bot_or_exists_atom_le _).resolve_left hbot
have ⟨hx, hy'⟩ := le_inf_iff.1 hle
have hy := h a ha hx
have : a ≤ y ⊓ yᶜ := le_inf_iff.2 ⟨hy, hy'⟩
ha.1 (by simpa using this)
exact (eq_compl_iff_isCompl.1 (by simp)).inf_right_eq_bot_iff.1 this
