dim_lt_of_lt — Mathlib

English

If x < y in X.N, then x.dim < y.dim; strict inequality of vertices implies strict inequality of dimensions.

Русский

Если x < y в X.N, тогда x.dim < y.dim; строгая неравенство вершин порождает строгое неравенство размерностей.

LaTeX

$$$ x < y \Rightarrow x.dim < y.dim $$$

Lean4

theorem dim_lt_of_lt {x y : X.N} (h : x < y) : x.dim < y.dim :=
  by
  obtain h' | h' := (dim_le_of_le h.le).lt_or_eq
  · exact h'
  · obtain ⟨f, _, hf⟩ := le_iff_exists_mono.1 h.le
    obtain ⟨d, ⟨x, hx⟩, rfl⟩ := x.mk_surjective
    obtain ⟨d', ⟨y, hy⟩, rfl⟩ := y.mk_surjective
    obtain rfl : d = d' := h'
    obtain rfl := SimplexCategory.eq_id_of_mono f
    obtain rfl : y = x := by simpa using hf
    simp at h

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