disjoint_upperClosure_left — Mathlib

English

For a lower set s and a set t, s.sdiff t is the largest lower subset of s that is disjoint from t.

Русский

Для нижнего множества s и множества t, s.sdiff t есть наибольшое по включению нижнее подмножество внутри s, не пересекающее t.

LaTeX

$$$ (s \\text{ sdiff } t) \\,=\, \\{ x \\in s : x \\notin \\operatorname{upperClosure}(t) \\} $$$

Lean4

@[simp]
theorem disjoint_upperClosure_left (ht : IsLowerSet t) : Disjoint (↑(upperClosure s)) t ↔ Disjoint s t :=
  by
  refine ⟨Disjoint.mono_left subset_upperClosure, ?_⟩
  simp only [disjoint_left, SetLike.mem_coe, mem_upperClosure, forall_exists_index, and_imp]
  exact fun h a b hb hba ha ↦ h hb <| ht hba ha

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