forall — Mathlib

English

For any property p on β, if hf and hf' hold, then (∀ y ∈ t, p(y)) ⇔ (∀ x ∈ s, p(f(x))).

Русский

Для любого свойства p на β, при выполнении hf и hf', верно (∀ y ∈ t, p(y)) ⇔ (∀ x ∈ s, p(f(x))).

LaTeX

$$$ (\forall y \in t, p(y)) \iff (\forall x \in s, p(f(x))) $$$

Lean4

theorem «forall» {p : β → Prop} (hf : s.SurjOn f t) (hf' : s.MapsTo f t) : (∀ y ∈ t, p y) ↔ (∀ x ∈ s, p (f x)) :=
  ⟨fun H x hx ↦ H (f x) (hf' hx), fun H _y hy ↦
    let ⟨x, hx, hxy⟩ := hf hy;
    hxy ▸ H x hx⟩

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