eq_of_one_to_two' — Mathlib

English

Refinement of the previous classification: f equals δ0, δ1, δ2, or is equal to mk 1 2 by a constant, with a layered disjunction.

Русский

Уточнение классификации: f равен δ0, δ1, δ2 или константному отображению через mk 1 на mk 2.

LaTeX

$$$\\forall f \\in \\mathrm{Hom} (\\mathrm{mk } 1, \\mathrm{mk } 2), \\ f = δ 0 \\lor f = δ 1 \\lor f = δ 2 \\lor \\exists a, f = (\\mathrm{mk } 1).\\const (\\mathrm{mk } 2) a$$$

Lean4

theorem eq_of_one_to_two' (f : ⦋1⦌ ⟶ ⦋2⦌) :
    f = (δ (n := 1) 0) ∨ f = (δ (n := 1) 1) ∨ f = (δ (n := 1) 2) ∨ ∃ a, f = SimplexCategory.const _ _ a :=
  match eq_of_one_to_two f with
  | .inl ⟨0, h⟩ => .inl h
  | .inl ⟨1, h⟩ => .inr (.inl h)
  | .inl ⟨2, h⟩ => .inr (.inr (.inl h))
  | .inr h => .inr (.inr (.inr h))

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