quotEquivOfEqBot_symm_apply — Mathlib

English

The inverse of the natural isomorphism between M/p and M, when p = ⊥, sends each x ∈ M to its coset in M/p; i.e., φ^{-1}(x) = [x].

Русский

Обратное к естественному изоморфизму между M/p и M, если p = ⊥, отправляет каждый элемент x ∈ M в его косет в M/p; то есть φ^{-1}(x) = [x].

LaTeX

$$$\forall p\subseteq M,\; p=\{0\} \Rightarrow \forall x\in M,\; (\varphi_p)^{-1}(x) = [x],$$$

Lean4

@[simp]
theorem quotEquivOfEqBot_symm_apply (hp : p = ⊥) (x : M) : (p.quotEquivOfEqBot hp).symm x = (Quotient.mk x) :=
  rfl

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