lift_lt_comp — Mathlib

English

Let a,b be elements of a generalized Boolean algebra. In the Booleanisation, lift(a) < comp(b) if and only if a and b are disjoint.

Русский

Пусть a и b — элементы обобщённой булевой алгебры. В буллизации, lift(a) < comp(b) тогда и только тогда, когда a и b не пересекаются.

LaTeX

$$$lift\ a < comp\ b \iff Disjoint\ a\ b$$$

Lean4

@[simp]
theorem lift_lt_comp : lift a < comp b ↔ Disjoint a b :=
  ⟨by rintro ⟨_⟩; assumption, LT.sep⟩

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