exists_ne — Mathlib

English

For a nontrivial α and injective f : α → β, for any y in β there exists x with f(x) ≠ y.

Русский

Для ненулевого α и инъекции f : α → β существует элемент x такой, что f(x) ≠ y для любого y ∈ β.

LaTeX

$$$\forall {\alpha} {\beta} [\mathrm{Nontrivial} \alpha] {f : \alpha \to \beta}, \mathrm{Injective} f \to \forall y, \exists x, f(x) \neq y$$$

Lean4

/-- An injective function from a nontrivial type has an argument at
which it does not take a given value. -/
protected theorem exists_ne [Nontrivial α] {f : α → β} (hf : Function.Injective f) (y : β) : ∃ x, f x ≠ y :=
  by
  rcases exists_pair_ne α with ⟨x₁, x₂, hx⟩
  by_cases h : f x₂ = y
  · exact ⟨x₁, (hf.ne_iff' h).2 hx⟩
  · exact ⟨x₂, h⟩

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