equivMapDomain_single — Mathlib

English

For f : α ≃ β, a ∈ α, b ∈ M, equivMapDomain f (single a b) = single (f a) b.

Русский

Для f : α ≃ β и элементa a ∈ α, b ∈ M, выполняется равенство equivMapDomain f (single a b) = single (f a) b.

LaTeX

$$equivMapDomain f (single a b) = single (f a) b$$

Lean4

@[simp]
theorem equivMapDomain_single (f : α ≃ β) (a : α) (b : M) : equivMapDomain f (single a b) = single (f a) b := by
  classical
  ext x
  simp only [single_apply, Equiv.apply_eq_iff_eq_symm_apply, equivMapDomain_apply]

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