nontrivial — Mathlib

English

If α is nontrivial and f : α → β is injective, then β is nontrivial.

Русский

Если α не тривиален и есть инъекция f : α → β, то β не тривиален.

LaTeX

$$$\forall {\alpha} {\beta} [\mathrm{Nontrivial} \alpha] {f : \alpha \to \beta}, \mathrm{Injective} f \to \mathrm{Nontrivial} \beta$$$

Lean4

/-- Pushforward a `Nontrivial` instance along an injective function. -/
protected theorem nontrivial [Nontrivial α] {f : α → β} (hf : Function.Injective f) : Nontrivial β :=
  let ⟨x, y, h⟩ := exists_pair_ne α
  ⟨⟨f x, f y, hf.ne h⟩⟩

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