le_iff_atom_le_imp — Mathlib

English

In a bottom-order atomistic poset, a ≤ b iff every atom c ≤ a implies c ≤ b.

Русский

В атомистичном порядке с нулем: a ≤ b тогда и только тогда, когда для всех атомов c, c ≤ a ⇒ c ≤ b.

LaTeX

$$$ a \\le b \\iff \\forall c : \\alpha, IsAtom c \\rightarrow c \\le a \\rightarrow c \\le b $$$

Lean4

theorem le_iff_atom_le_imp {a b : α} : a ≤ b ↔ ∀ c : α, IsAtom c → c ≤ a → c ≤ b :=
  ⟨fun hab _ _ hca ↦ hca.trans hab, fun h ↦ (isLUB_atoms_le a).mono (isLUB_atoms_le b) fun _ ⟨h₁, h₂⟩ ↦ ⟨h₁, h _ h₁ h₂⟩⟩

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