insert_apply_left — Mathlib

English

For a not in s, the forward map of insert yields the opposite of Sum.inr unit.

Русский

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

LaTeX

$$insert H ⟨a, inl rfl⟩ = Sum.inr PUnit.unit$$

Lean4

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

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