codisjoint_iff

Mathlib.Order.CompleteSublattice

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

← MathLib Explorer

English

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

Русский

Кодисоединение пары в L эквивалентно кодисоединению в α.

LaTeX

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

Lean4

protected theorem codisjoint_iff {a b : L} : Codisjoint a b ↔ Codisjoint (a : α) (b : α) := by
  rw [codisjoint_iff, codisjoint_iff, ← Sublattice.coe_sup, ← coe_top (L := L), Subtype.coe_injective.eq_iff]

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

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

Разделы

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

Аффилиация

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