sumDiffSubset — Mathlib

English

There is a natural equivalence between s ⊕ (t \ s) and t, given s ⊆ t.

Русский

Существует естественная эквивалентность между s ⊕ (t \ s) и t, если s ⊆ t.

LaTeX

$$s ⊕ (t \ s) ≃ t$$

Lean4

/-- `sumDiffSubset s t` is the natural equivalence between
`s ⊕ (t \ s)` and `t`, where `s` and `t` are two sets. -/
protected def sumDiffSubset {α} {s t : Set α} (h : s ⊆ t) [DecidablePred (· ∈ s)] : s ⊕ (t \ s : Set α) ≃ t :=
  calc
    s ⊕ (t \ s : Set α) ≃ (s ∪ t \ s : Set α) := (Equiv.Set.union disjoint_sdiff_self_right).symm
    _ ≃ t := Equiv.setCongr (by simp [union_diff_self, union_eq_self_of_subset_left h])

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