insert_apply_right — Mathlib

English

For a not in s, the forward map of insert yields Sum.inl b for b ∈ s.

Русский

При отсутствии элемента в s, передающее отображение вставки даёт Sum.inl b для b ∈ s.

LaTeX

$$insert H ⟨b, inr b.2⟩ = Sum.inl b$$

Lean4

@[simp]
theorem insert_apply_right {α} {s : Set.{u} α} [DecidablePred (· ∈ s)] {a : α} (H : a ∉ s) (b : s) :
    Equiv.Set.insert H ⟨b, Or.inr b.2⟩ = Sum.inl b :=
  (Equiv.Set.insert H).apply_eq_iff_eq_symm_apply.2 rfl

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