dualQuotEquivDualAnnihilator_symm_apply_mk

English

For W, φ ∈ (M/W)^*, and x ∈ M, the application of the equivalence to φ and Quotient.mk x yields φ(x).

Русский

Для W, φ ∈ (M/W)^*, и x ∈ M, применение эквивалента к φ на Quotient.mk x равно φ(x).

LaTeX

$$$W.dualQuotEquivDualAnnihilator(φ)(\overline{x}) = φ(x)$$$

Lean4

@[simp]
theorem dualQuotEquivDualAnnihilator_symm_apply_mk (W : Submodule R M) (φ : W.dualAnnihilator) (x : M) :
    (dualQuotEquivDualAnnihilator W).symm φ (Quotient.mk x) = φ x :=
  rfl

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