degenerate_le_preimage — Mathlib

English

For any morphism f: X → Y, the degenerate simplices X.degenerate(n) are contained in the preimage of Y.degenerate(n) under f.app.

Русский

Для отображения f: X → Y множество вырожденных симпликсов X включено в предобраз f.app^{-1}(Y.degenerate(n)).

LaTeX

$$$$X.degenerate(n) \subseteq (f.app _)^{-1}(Y.degenerate(n)),$$$$

Lean4

theorem degenerate_le_preimage (f : X ⟶ Y) (n : ℕ) : X.degenerate n ⊆ (f.app _) ⁻¹' (Y.degenerate n) := fun _ hx ↦
  degenerate_app_apply hx f

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