forall — Mathlib

English

If f is surjective, then (forall y, p(y)) iff (forall x, p(f(x))).

Русский

Если f сюръективна, то (для всех y) p(y) эквивалентно (для всех x) p(f(x)).

LaTeX

$$$\\operatorname{Surjective}(f) \\rightarrow (\\forall y\\, p(y) \\iff \\forall x\\, p(f(x)))$$$

Lean4

protected theorem «forall» (hf : Surjective f) {p : β → Prop} : (∀ y, p y) ↔ ∀ x, p (f x) :=
  ⟨fun h x ↦ h (f x), fun h y ↦
    let ⟨x, hx⟩ := hf y
    hx ▸ h x⟩

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