exists_le_covBy_of_lt

Mathlib.Order.Atoms

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

English

In a strongly coatomic poset, if a < b, there exists x with a ≤ x and x ⋖ b.

Русский

В сильно коатомном порядке, если a < b, существует x с a ≤ x и x ⋖ b.

LaTeX

$$$ [IsStronglyCoatomic α] (a < b) \rightarrow \exists x, a \le x \land x \,⋖\, b $$$

Lean4

theorem exists_le_covBy_of_lt [IsStronglyCoatomic α] (h : a < b) : ∃ x, a ≤ x ∧ x ⋖ b :=
  IsStronglyCoatomic.exists_le_covBy_of_lt a b h

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

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

Разделы

Аффилиация

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