disjoint_upperClosure_right — Mathlib

English

If t is a lower set, then the disjointness of the upper closure of s with t is equivalent to the disjointness of s with t.

Русский

Если t — нижнее множество, то нес пересечение верхнего замыкания s с t эквивалентно нес пересечению s и t.

LaTeX

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

Lean4

@[simp]
theorem disjoint_upperClosure_right (hs : IsLowerSet s) : Disjoint s (upperClosure t) ↔ Disjoint s t := by
  simpa only [disjoint_comm] using hs.disjoint_upperClosure_left

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