exists_mem_image2 — Mathlib

English

There exists z ∈ image2 f s t with p z if and only if there exist x ∈ s and y ∈ t such that p (f x y).

Русский

Существует z ∈ image2 f s t с свойством p, если и только если существуют x ∈ s и y ∈ t такие, что p (f x y).

LaTeX

$$∃ z ∈ image2 f s t, p z ↔ ∃ x ∈ s, ∃ y ∈ t, p (f x y).$$

Lean4

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

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