eq_or_len_le_of_P_δ — Mathlib

English

For any f with P_δ, either f is an isomorphism (f = eqToHom h) or x.len < y.len.

Русский

Для любого morphism f с P_δ либо f является изоморфизмом, либо длина области меньше длины кода.

LaTeX

$$(∃ h, f = eqToHom h) ∨ x.len < y.len$$

Lean4

theorem eq_or_len_le_of_P_δ {x y : SimplexCategoryGenRel} {f : x ⟶ y} (h_δ : P_δ f) :
    (∃ h : x = y, f = eqToHom h) ∨ x.len < y.len := by
  induction h_δ with
  | of _ hx => cases hx; right; simp
  | id => left; use rfl; simp
  | comp_of i u _ hg h' =>
    rcases h' with ⟨e, _⟩ | h' <;> apply Or.inr <;> cases hg
    · rw [e]
      exact Nat.lt_add_one _
    · exact Nat.lt_succ_of_lt h'

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