isCompl_iff

Mathlib.Order.CompleteSublattice

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

← MathLib Explorer

English

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

Русский

IsCompl в L эквивалентно IsCompl в α.

LaTeX

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

Lean4

protected theorem isCompl_iff {a b : L} : IsCompl a b ↔ IsCompl (a : α) (b : α) := by
  rw [isCompl_iff, isCompl_iff, CompleteSublattice.disjoint_iff, CompleteSublattice.codisjoint_iff]

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

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

Разделы

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

Аффилиация

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