union_apply_left — Mathlib

English

In the canonical bijection between s ∪ t and s ⊕ t, an element coming from s maps to the left component.

Русский

В канонической биекции между s ∪ t и s ⊕ t элемент, принадлежащий s, попадает в левый компонент.

LaTeX

$$For any $a\in s$, $f(a)=\mathrm{inl}(a)$ where $f:(s\cup t)\to s\oplus t$ is the union bijection.$$

Lean4

theorem union_apply_left {α} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t) {a : (s ∪ t : Set α)}
    (ha : ↑a ∈ s) : Equiv.Set.union H a = Sum.inl ⟨a, ha⟩ :=
  dif_pos ha

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