le_iff_exists_mono — Mathlib

English

For nondegenerate x ≤ y in X.N, there exists a mono morphism f between the corresponding simplices such that X.map f.op y.simplex = x.simplex.

Русский

Если x ≤ y в X.N неdegenerate, то существует монообразование f между соответствующими симплексами так, что X.map f.op y.simplex = x.simplex.

LaTeX

$$$ x \le y \iff \exists f : ⟦x.dim⟧ ⟶ ⟦y.dim⟧\; (Mono\; f) \land X.map f.op y.simplex = x.simplex $$$

Lean4

theorem le_iff_exists_mono {x y : X.N} :
    x ≤ y ↔ ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌) (_ : Mono f), X.map f.op y.simplex = x.simplex :=
  by
  simp only [le_iff, CategoryTheory.Subpresheaf.ofSection_le_iff, Subcomplex.mem_ofSimplex_obj_iff]
  exact ⟨fun ⟨f, hf⟩ ↦ ⟨f, X.mono_of_nonDegenerate ⟨_, x.nonDegenerate⟩ f _ hf, hf⟩, by tauto⟩

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