union_apply_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem union_apply_right {α} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t) {a : (s ∪ t : Set α)}
    (ha : ↑a ∈ t) : Equiv.Set.union H a = Sum.inr ⟨a, ha⟩ :=
  dif_neg fun h => Set.disjoint_left.mp H h ha

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