extChartAt_inl_apply — Mathlib

English

Compatibility of extended charts with left injection: extChartAt I (Sum.inl x) applied to Sum.inl y equals extChartAt I x applied to y.

Русский

Совместимость расширенных диаграмм с векторной вставкой: extChartAt I (Sum.inl x) (Sum.inl y) = extChartAt I x y.

LaTeX

$$$ (extChartAt I (Sum.inl x)) (Sum.inl y) = (extChartAt I x) y $$$

Lean4

theorem extChartAt_inl_apply {x y : M} : (extChartAt I (.inl x : M ⊕ M')) (Sum.inl y) = (extChartAt I x) y := by simp

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