quotientInfEquivSupQuotient_surjective

English

The equation matching (between quotientInfToSupQuotient and quotientInfEquivSupQuotient) holds in the first two indices.

Русский

Соответствие между quotientInfToSupQuotient и quotientInfEquivSupQuotient выполняется в первых двух индексаx.

LaTeX

$$quotientInfEquivSupQuotient_match_1_2 p p' (motive) (x) (hx) => ...$$

Lean4

theorem quotientInfEquivSupQuotient_surjective (p p' : Submodule R M) :
    Function.Surjective (quotientInfToSupQuotient p p') :=
  by
  rw [← range_eq_top, quotientInfToSupQuotient, range_liftQ, eq_top_iff']
  rintro ⟨x, hx⟩; rcases mem_sup.1 hx with ⟨y, hy, z, hz, rfl⟩
  use ⟨y, hy⟩; apply (Submodule.Quotient.eq _).2
  simp only [mem_comap, map_sub, coe_subtype, coe_inclusion, sub_add_cancel_left, neg_mem_iff, hz]

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