unique_nonDegenerate_simplex — Mathlib

English

The non-degenerate representation of x is unique up to equalities of the same dimension.

Русский

У представления x через недегенеративные данные уникальность по размерности сохраняется.

LaTeX

$$$ \forall x, \forall f_1, y_1, \forall f_2, y_2, \big( x = X.map f_1.op y_1 = X.map f_2.op y_2 \Rightarrow y_1 = y_2 \big) $$$

Lean4

theorem unique_nonDegenerate_simplex (x : X _⦋n⦌) {m : ℕ} (f₁ : ⦋n⦌ ⟶ ⦋m⦌) [Epi f₁] (y₁ : X.nonDegenerate m)
    (hy₁ : x = X.map f₁.op y₁) (f₂ : ⦋n⦌ ⟶ ⦋m⦌) (y₂ : X.nonDegenerate m) (hy₂ : x = X.map f₂.op y₂) : y₁ = y₂ :=
  by
  obtain ⟨⟨hf₁⟩⟩ := isSplitEpi_of_epi f₁
  ext
  simpa [g_eq_id hy₁ hy₂ hf₁] using (map_g_op_y₂ hf₁ hy₁ hy₂).symm

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