forall_mem_image2 — Mathlib

English

For every p : γ → Prop, (∀ z ∈ image2 f s t, p z) is equivalent to ∀ x ∈ s, ∀ y ∈ t, p (f x y).

Русский

Для любого p: γ → Prop выполняется эквивалентность: ∀ z ∈ image2 f s t, p z ⇔ ∀ x ∈ s, ∀ y ∈ t, p (f x y).

LaTeX

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

Lean4

theorem forall_mem_image2 {p : γ → Prop} : (∀ z ∈ image2 f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y) := by aesop

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