eq_of_one_to_one — Mathlib

English

A morphism ⦋1⦌ ⟶ ⦋1⦌ is either constant or the identity; no other possibilities occur.

Русский

Морфизм ⦋1⦌ ⟶ ⦋1⦌ либо константен, либо равен тождественному, других вариантов нет.

LaTeX

$$$\\forall f:\\; \\lbrack 1 \\rbrack \\to \\lbrack 1 \\rbrack,\n\\; (\\exists a, f = const \\lbrack 1 \\rbrack \\_ a) \\lor f = \\mathrm{id}.$$$

Lean4

theorem eq_of_one_to_one (f : ⦋1⦌ ⟶ ⦋1⦌) : (∃ a, f = const ⦋1⦌ _ a) ∨ f = 𝟙 _ := by
  match e0 : f.toOrderHom 0, e1 : f.toOrderHom 1 with
  | 0, 0 | 1, 1 =>
    refine .inl ⟨f.toOrderHom 0, ?_⟩
    ext i : 3
    match i with
    | 0 => rfl
    | 1 => exact e1.trans e0.symm
  | 0, 1 =>
    right
    ext i : 3
    match i with
    | 0 => exact e0
    | 1 => exact e1
  | 1, 0 =>
    have := f.toOrderHom.monotone (by decide : (0 : Fin 2) ≤ 1)
    rw [e0, e1] at this
    exact Not.elim (by decide) this

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