mk_map_le — Mathlib

English

For x ∈ X.S at dimension n and f: ⟨m⟧ ⟶ ⟨n⟧, we have S.mk(X.map f.op x) ≤ S.mk x; i.e., pushing forward cannot increase the subcomplex.

Русский

Для x ∈ X.S размерности n и f: ⟨m⟧ ⟶ ⟨n⟧ имеет место, что S.mk(X.map f.op x) ≤ S.mk x; то есть перенос поображения не увеличивает подслой.

LaTeX

$$$S.mk\,(X.map\ f.op\ x) \le S.mk\ x$$$

Lean4

theorem mk_map_le {n m : ℕ} (x : X _⦋n⦌) (f : ⦋m⦌ ⟶ ⦋n⦌) : S.mk (X.map f.op x) ≤ S.mk x :=
  by
  rw [le_iff]
  tauto

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