disjoint_iff

Mathlib.Order.CompleteSublattice

URI: https://scilib.ai/kg/mathlib#CompleteSublattice.disjoint_iff

← MathLib Explorer

English

Disjoint a b in L iff Disjoint (a, b) in α.

Русский

Разбиение ∅(a,b) в L эквивалентно разбиению в α.

LaTeX

$$Disjoint a b ↔ Disjoint (a : α) (b : α)$$

Lean4

protected theorem disjoint_iff {a b : L} : Disjoint a b ↔ Disjoint (a : α) (b : α) := by
  rw [disjoint_iff, disjoint_iff, ← Sublattice.coe_inf, ← coe_bot (L := L), Subtype.coe_injective.eq_iff]

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

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

Разделы

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

Аффилиация

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