sdiff_inf_upperClosure — Mathlib

English

If t ⊆ s and t is closed upward relative to s, then (s \lowerClosure t) ∩ upperClosure t = s.

Русский

Если t ⊆ s и t замкнуто сверху относительно s, то (s \\lowerClosure(t)) ∩ upperClosure(t) = s.

LaTeX

$$$ (s \\operatorname{lowerClosure}(t)) \\cap \\operatorname{upperClosure}(t) = s $$$

Lean4

theorem sdiff_inf_upperClosure (hts : t ⊆ s) (hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) : s.sdiff t ⊓ upperClosure t = s :=
  by
  refine ge_antisymm (le_inf le_sdiff_left <| le_upperClosure.2 hts) fun a ha ↦ ?_
  obtain hat | hat := em (a ∈ t)
  · exact subset_union_right (subset_upperClosure hat)
  · refine subset_union_left ⟨ha, ?_⟩
    rintro ⟨b, hb, hab⟩
    exact hat <| hst _ ha _ hb hab

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