isCoatom_iff_eq_bot

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#isCoatom_iff_eq_bot

English

An element is a coatom iff it equals the bottom.

Русский

Элемент является коатомом тогда и только тогда, когда он равен нижней границе.

LaTeX

$$$\text{IsCoatom}(a) \iff a = \bot$$$

Lean4

@[simp]
theorem isCoatom_iff_eq_bot {a : α} : IsCoatom a ↔ a = ⊥ :=
  ⟨fun h ↦ (eq_bot_or_eq_top a).resolve_right h.1, (· ▸ isCoatom_bot)⟩

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

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

Разделы

Аффилиация

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