disjoint_of_subsingleton — Mathlib

English

In a lattice with a bottom element, any two elements are disjoint if the carrier is a singleton.

Русский

В решётке с нулём любыe два элемента являются взаимоисключающими, если множество данных подмножество схлопывается к одному элементу.

LaTeX

$$$Disjoint a b$ holds in a subsingleton, i.e., $Subsingleton \\alpha$ implies $Disjoint a b$$$

Lean4

@[simp]
theorem disjoint_of_subsingleton [Subsingleton α] : Disjoint a b := fun x _ _ ↦ le_of_eq (Subsingleton.elim x ⊥)

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