degenerate_iff_of_mono — Mathlib

English

Let f: X → Y be mono. Then for every n and x ∈ X.obj(n), f.app(x) ∈ Y.degenerate(n) iff x ∈ X.degenerate(n).

Русский

Пусть f: X → Y — моно. Тогда для всякого n и x ∈ X.obj(n): f.app(x) ∈ degenerate(n) iff x ∈ degenerate(n).

LaTeX

$$$$\text{Mono}(f) \Rightarrow (f.app_{n}(x) \in Y_{\mathrm{deg}}(n) \iff x \in X_{\mathrm{deg}}(n)),$$$$

Lean4

theorem degenerate_iff_of_mono {Y : SSet.{u}} (f : X ⟶ Y) [Mono f] (x : X _⦋n⦌) :
    f.app _ x ∈ Y.degenerate n ↔ x ∈ X.degenerate n :=
  by
  rw [← degenerate_iff_of_isIso (Subcomplex.toRange f) x, Subcomplex.mem_degenerate_iff]
  simp

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