factor_comp_mk — Mathlib

English

The composition of two quotient factors equals the quotient factor of the composed inclusions: (factor H2) ∘ (factor H1) = factor (H1.trans H2).

Русский

Сочетание двух факторных отображений равно факторному отображению от объединения подмодулей: (factor H2) ∘ (factor H1) = factor (H1.trans H2).

LaTeX

$$$$ (\\text{factor} \\, H2) .\\text{comp} (\\text{factor} \\, H1) = \\text{factor} \\,(H1.trans H2). $$$$

Lean4

@[simp]
theorem factor_comp_mk (H : p ≤ p') : (factor H).comp (mkQ p) = mkQ p' :=
  by
  ext x
  rw [LinearMap.comp_apply, factor_mk]

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