lt_iff — Mathlib

English

Let α be a partial order with a top element ⊤, and let a be a coatom. Then for every x, a < x if and only if x = ⊤.

Русский

Пусть α — частичный порядок с верхним элементом ⊤, и a — коатом. Тогда для любого x выполняется a < x тогда и только если x = ⊤.

LaTeX

$$$ \\mathrm{IsCoatom}(a) \\rightarrow \\forall x\\,(a < x \\leftrightarrow x = \\top).$$$

Lean4

theorem lt_iff (h : IsCoatom a) : a < x ↔ x = ⊤ :=
  h.dual.lt_iff

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