sUnion_insert_disjointOfDiff — Mathlib

English

If t ⊆ s and s,t ∈ C, then the union over insert t (hC.disjointOfDiff hs ht) recovers s.

Русский

Если t ⊆ s и s,t ∈ C, то объединение множества insert t (hC.disjointOfDiff hs ht) даёт с повторно s.

LaTeX

$$$$ ⋃_0 \\text{insert } t (hC.disjointOfDiff hs ht) = s $$$$

Lean4

theorem sUnion_insert_disjointOfDiff (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) (hst : t ⊆ s) :
    ⋃₀ insert t (hC.disjointOfDiff hs ht) = s :=
  by
  conv_rhs => rw [← union_diff_cancel hst, ← hC.sUnion_disjointOfDiff hs ht]
  simp only [sUnion_insert]

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