quotientInfEquivSupQuotient_apply_mk

English

Applying quotientInfEquivSupQuotient to mk x yields the canonical quotient.

Русский

Применение quotientInfEquivSupQuotient к mk x даёт канонический фактор.

LaTeX

$$theorem quotientInfEquivSupQuotient_apply_mk (p p' : Submodule R M) (x : Subtype fun x => SetLike.instMembership.mem p x) : quotientInfEquivSupQuotient p p' (Submodule.Quotient.mk x) = Submodule.Quotient.mk (LinearMap.instFunLike.coe (Submodule.inclusion) x)$$

Lean4

theorem quotientInfEquivSupQuotient_apply_mk (p p' : Submodule R M) (x : p) :
    let map := inclusion (le_sup_left : p ≤ p ⊔ p')
    quotientInfEquivSupQuotient p p' (Submodule.Quotient.mk x) =
      @Submodule.Quotient.mk R (p ⊔ p' : Submodule R M) _ _ _ (comap (p ⊔ p').subtype p') (map x) :=
  rfl

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