degenerate_eq_iUnion_range_σ — Mathlib

English

The set of degenerate (n+1)-simplices is the union over i of the ranges of σ_i.

Русский

Множество дегenerate (n+1)-симплексoв равно объединению по i образов σ_i.

LaTeX

$$$ X.degenerate(n+1) = \bigcup_{i: \mathrm{Fin}(n+1)} \mathrm{range}(X.\sigma i) $$$

Lean4

theorem degenerate_eq_iUnion_range_σ : X.degenerate (n + 1) = ⋃ (i : Fin (n + 1)), Set.range (X.σ i) :=
  by
  ext x
  constructor
  · intro hx
    rw [mem_degenerate_iff] at hx
    obtain ⟨m, hm, f, hf, y, rfl⟩ := hx
    obtain ⟨i, θ, rfl⟩ :=
      SimplexCategory.eq_σ_comp_of_not_injective f
        (fun hf ↦ by
          rw [← SimplexCategory.mono_iff_injective] at hf
          have := SimplexCategory.le_of_mono f
          cutsat)
    aesop
  · intro hx
    simp only [Set.mem_iUnion, Set.mem_range] at hx
    obtain ⟨i, y, rfl⟩ := hx
    apply σ_mem_degenerate

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