exists_mem_image₂ — Mathlib

English

Let p be a predicate on γ. Then there exists z in the image_2 f s t such that p(z) holds if and only if there exist x ∈ s and y ∈ t with p(f(x,y)).

Русский

Пусть p : γ → ⟂. Тогда существует z ∈ образ_2 f s t такое, что p(z) выполняется тогда и только тогда существуют x ∈ s и y ∈ t такие, что p(f(x,y)).

LaTeX

$$$\\exists z \\in \\operatorname{image}_2 f\, s\, t\\, p(z) \\iff \\exists x \\in s \\;\\exists y \\in t\\; p(f(x,y))$$$

Lean4

theorem exists_mem_image₂ {p : γ → Prop} : (∃ z ∈ image₂ f s t, p z) ↔ ∃ x ∈ s, ∃ y ∈ t, p (f x y) := by
  simp_rw [← mem_coe, coe_image₂, exists_mem_image2]

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