disjoint_lowerClosure_right — Mathlib

English

For an IsUpperSet s, Disjoint (LowerSet.coe (lowerClosure s)) t ↔ Disjoint s t.

Русский

Для верхнего множества s верно, что Disjoint(LowerSet.coe(lowerClosure s), t) эквивалентно Disjoint(s,t).

LaTeX

$$$ \\operatorname{Disjoint}(\\operatorname{LowerSet.coe}(\\operatorname{lowerClosure}(s)), t) \\iff \\operatorname{Disjoint}(s, t) $$$

Lean4

@[simp]
theorem disjoint_lowerClosure_right (hs : IsUpperSet s) : Disjoint s (lowerClosure t) ↔ Disjoint s t :=
  hs.toDual.disjoint_upperClosure_right

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