le_iff

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#IsCoatom.le_iff

English

If a is a coatom, then for any x, a ≤ x holds exactly when x = ⊤ or x = a.

Русский

Пусть a — коатом. Тогда для любого x верно: a ≤ x тогда, когда x = ⊤ или x = a.

LaTeX

$$$ \\mathrm{IsCoatom}(a) \\rightarrow (a \\le x \\leftrightarrow x = \\top \\lor x = a).$$$

Lean4

theorem le_iff (h : IsCoatom a) : a ≤ x ↔ x = ⊤ ∨ x = a :=
  h.dual.le_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru