eq_iff_atom_le_iff — Mathlib

English

Equality x = y is equivalent to atom-le-imp characterizations: for all atoms a, a ≤ x iff a ≤ y.

Русский

Равенство x = y эквивалентно характеристике через атомы: для всех атомов a выполняется a ≤ x ⇔ a ≤ y.

LaTeX

$$$ a = b \\iff \\forall c, IsAtom c \\rightarrow (c \\le a \\iff c \\le b)$$$

Lean4

theorem eq_iff_atom_le_iff {a b : α} : a = b ↔ ∀ c, IsAtom c → (c ≤ a ↔ c ≤ b) :=
  by
  refine ⟨fun h => by simp [h], fun h => ?_⟩
  rw [le_antisymm_iff, le_iff_atom_le_imp, le_iff_atom_le_imp]
  simp_all

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