nonDegenerate_iff_of_mono — Mathlib

English

If f: X → Y is mono, then x is nondegenerate in X exactly when f.app(x) is nondegenerate in Y.

Русский

Если f: X → Y моно, то x ненегидна в X тогда и только тогда, когда f.app(x) ненегидна в Y.

LaTeX

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

Lean4

theorem nonDegenerate_iff_of_mono {Y : SSet.{u}} (f : X ⟶ Y) [Mono f] (x : X _⦋n⦌) :
    f.app _ x ∈ Y.nonDegenerate n ↔ x ∈ X.nonDegenerate n := by
  simp [mem_nonDegenerate_iff_notMem_degenerate, degenerate_iff_of_mono]

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