len_lt_of_mono — Mathlib

English

If i: Δ' ⟶ Δ is mono and Δ ≠ Δ', then Δ'.len < Δ.len.

Русский

Если i: Δ' ⟶ Δ моно и Δ ≠ Δ', то Δ'.len < Δ.len.

LaTeX

$$$\\\\forall {\\\\Delta' \\\\Delta} (i: \\\\Delta' \\\\to \\\\Delta) [Mono i], \\\\Delta \\\\neq \\\\Delta' \\\Rightarrow \\\\Delta'.len < \\\\Delta.len$$$

Lean4

theorem len_lt_of_mono {Δ' Δ : SimplexCategory} (i : Δ' ⟶ Δ) [Mono i] (hi' : Δ ≠ Δ') : Δ'.len < Δ.len := by
  grind [→ len_le_of_mono, SimplexCategory.ext]

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