disjoint_lowerClosure_left — Mathlib

English

If s is a lower set, then Disjoint(s, upperClosure(t)) is equivalent to Disjoint(s, t).

Русский

Если s — нижнее множество, то Disjoint(s, upperClosure(t)) эквивалентно Disjoint(s, t).

LaTeX

$$$ \\operatorname{Disjoint}(s, \\operatorname{upperClosure}(t)) \\iff \\operatorname{Disjoint}(s, t) $$$

Lean4

@[simp]
theorem disjoint_lowerClosure_left (ht : IsUpperSet t) : Disjoint (↑(lowerClosure s)) t ↔ Disjoint s t :=
  ht.toDual.disjoint_upperClosure_left

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