codisjoint_iff

Mathlib.Order.LatticeIntervals

URI: https://scilib.ai/kg/mathlib#Set.Ioc.codisjoint_iff

← MathLib Explorer

English

For x,y ∈ Ioc(a,b), Codisjoint x y iff x ⊔ y = b in α.

Русский

Для x,y ∈ Ioc(a,b) кодиссjoint равносилен x ⊔ y = b в α.

LaTeX

$$$[SemilatticeSup\\;α] {a\\,b:\\alpha} [Fact (a

Lean4

protected theorem codisjoint_iff [SemilatticeSup α] {a b : α} [Fact (a < b)] {x y : Ioc a b} :
    Codisjoint x y ↔ ↑x ⊔ ↑y = b := by simp [_root_.codisjoint_iff, Subtype.ext_iff]

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

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

Разделы

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

Аффилиация

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