nontrivial — Mathlib

English

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

Русский

Если β не тривиална и f: α → β сюръективна, тогда α не тривиален.

LaTeX

$$$\text{Nontrivial}(\beta) \Rightarrow \bigl(\text{Surjective}(f) \Rightarrow \text{Nontrivial}(\alpha)\bigr)$$$

Lean4

/-- Pullback a `Nontrivial` instance along a surjective function. -/
protected theorem nontrivial [Nontrivial β] {f : α → β} (hf : Function.Surjective f) : Nontrivial α :=
  by
  rcases exists_pair_ne β with ⟨x, y, h⟩
  rcases hf x with ⟨x', hx'⟩
  rcases hf y with ⟨y', hy'⟩
  have : x' ≠ y' := by
    refine fun H ↦ h ?_
    rw [← hx', ← hy', H]
  exact ⟨⟨x', y', this⟩⟩

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