sdiff_sup_lowerClosure — Mathlib

English

If t ⊆ s and whenever b ∈ s and c ∈ t with c ≤ b then b ∈ t, then s equals the sup of sdiff t and lowerClosure t.

Русский

При условии, что t ⊆ s и если b ∈ s и c ∈ t с условием c ≤ b, то b ∈ t, тогда s = (s \ upperClosure t) ⊔ lowerClosure t.

LaTeX

$$$ s \\text{ sdiff } t \\;\\;\\sqcup \\;\\lowerClosure(t) = s $$$

Lean4

theorem sdiff_sup_lowerClosure (hts : t ⊆ s) (hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t) : s.sdiff t ⊔ lowerClosure t = s :=
  by
  refine le_antisymm (sup_le sdiff_le_left <| lowerClosure_le.2 hts) fun a ha ↦ ?_
  obtain hat | hat := em (a ∈ t)
  · exact subset_union_right (subset_lowerClosure hat)
  · refine subset_union_left ⟨ha, ?_⟩
    rintro ⟨b, hb, hba⟩
    exact hat <| hst _ ha _ hb hba

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