le_iff — Mathlib

English

For any s,t in X.S, s ≤ t if and only if there exists a morphism f: ⟨s.dim⟩ ⟶ ⟨t.dim⟩ such that X.map f.op t.simplex = s.simplex.

Русский

Для любых s,t в X.S, s ≤ t тогда и только тогда, когда существует морфизм f: ⟨s.dim⟩ ⟶ ⟨t.dim⟩ такой, что X.map f.op t.simplex = s.simplex.

LaTeX

$$$s \le t \iff \exists f:\; ⟨s.dim⟩ ⟶ ⟨t.dim⟩,\ X.map f.op\ t.simplex = s.simplex$$$

Lean4

theorem le_iff {s t : X.S} : s ≤ t ↔ ∃ (f : ⦋s.dim⦌ ⟶ ⦋t.dim⦌), X.map f.op t.simplex = s.simplex :=
  by
  rw [le_def, Subcomplex.ofSimplex_le_iff, Subpresheaf.ofSection_obj, Set.mem_setOf_eq]
  tauto

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