quotientInfEquivSupQuotient_symm_apply_left

English

Equivalence symmetry yields that the inverse image is zero iff x ∈ p'.

Русский

Симметрия эквивалентности: обратное изображение равно нулю тогда и только тогда, когда x ∈ p'.

LaTeX

$$theorem quotientInfEquivSupQuotient_symm_apply_eq_zero_iff {p p' : Submodule R M} {x : Subtype fun x => SetLike.instMembership.mem (SemilatticeSup.toMax.max p p') x} : (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = 0 ↔ (x : M) ∈ p'$$

Lean4

theorem quotientInfEquivSupQuotient_symm_apply_left (p p' : Submodule R M) (x : ↥(p ⊔ p')) (hx : (x : M) ∈ p) :
    (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨x, hx⟩ :=
  (LinearEquiv.symm_apply_eq _).2 <| by rw [quotientInfEquivSupQuotient_apply_mk, inclusion_apply]

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