dimension_comp_eq_dimension_add_dimension

English

The dimension of the composition equals the sum of the dimensions of the components.

Русский

Размерность композиции равна сумме размерностей компонент.

LaTeX

$$dimension (Q.comp P) = dimension(Q) + dimension(P)$$

Lean4

/-- The dimension of the composition of two finite submersive presentations is
the sum of the dimensions. -/
theorem dimension_comp_eq_dimension_add_dimension [Finite ι] [Finite ι'] [Finite σ] [Finite σ'] :
    (Q.comp P).dimension = Q.dimension + P.dimension :=
  by
  simp only [Presentation.dimension]
  have : Nat.card σ ≤ Nat.card ι := card_relations_le_card_vars_of_isFinite P
  have : Nat.card σ' ≤ Nat.card ι' := card_relations_le_card_vars_of_isFinite Q
  simp only [Nat.card_sum]
  cutsat

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