factorsThruAlong_id — Mathlib

English

For any X and presieve S and T, S.FactorsThruAlong T (id X) is equivalent to S.FactorsThru T.

Русский

Для любого X и пресивеза S, T выполняется эквивалентность S.FactorsThruAlong (id X) T и S.FactorsThru T.

LaTeX

$$$S.FactorsThruAlong T (\mathrm{id}_X) \iff S.FactorsThru T$$$

Lean4

@[simp]
theorem factorsThruAlong_id {X : C} (S T : Presieve X) : S.FactorsThruAlong T (𝟙 X) ↔ S.FactorsThru T := by
  simp [FactorsThruAlong, FactorsThru]

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