disjoint_compl_right_iff

Mathlib.Order.Heyting.Regular

URI: https://scilib.ai/kg/mathlib#Heyting.IsRegular.disjoint_compl_right_iff

← MathLib Explorer

English

For a regular b, Disjoint a bᶜ iff a ≤ b.

Русский

Для регулярного b: Disjoint a bᶜ эквивалентно a ≤ b.

LaTeX

$$$\forall a,b:\alpha,\ \mathrm{IsRegular}(b)\to\mathrm{Disjoint}(a,b^c)\iff a\le b$$$

Lean4

protected theorem disjoint_compl_right_iff (hb : IsRegular b) : Disjoint a bᶜ ↔ a ≤ b := by
  rw [← le_compl_iff_disjoint_right, hb.eq]
    -- See note [reducible non-instances]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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