const_injective — Mathlib

English

If α is nonempty, the constant-at-α map β → α → β is injective.

Русский

Если α непусто, отображение константности β в α → β инъективно.

LaTeX

$$$$\\\\forall b_1,b_2:\\\\beta, (\\\\mathrm{const}_{\\\\alpha}(b_1) = \\\\mathrm{const}_{\\\\alpha}(b_2)) \\\\Rightarrow b_1 = b_2. $$$$

Lean4

theorem const_injective [Nonempty α] : Injective (const α : β → α → β) := fun _ _ h ↦
  let ⟨x⟩ := ‹Nonempty α›
  congr_fun h x

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