union — Mathlib

English

If s and t are disjoint, then s ∪ t is bijective to s ⊕ t.

Русский

Если s и t не пересекаются, то их объединение s ∪ t эквивалентно дизъюнкции s ⊕ t.

LaTeX

$$$(s \cup t) \cong s \oplus t$$$

Lean4

/-- If sets `s` and `t` are disjoint, then `s ∪ t` is equivalent to `s ⊕ t`. -/
protected def union {α} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t) : (s ∪ t : Set α) ≃ s ⊕ t :=
  Set.union' (fun x => x ∈ s) (fun _ => id) fun _ xt xs => Set.disjoint_left.mp H xs xt

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