forall_mem_image₂ — Mathlib

English

A property holds for all elements of image₂ f s t if and only if it holds for all f a b with a ∈ s and b ∈ t.

Русский

Свойство справедливо для всех элементов image₂ f s t тогда и только тогда, когда оно верно для всех f(a,b) с a∈s, b∈t.

LaTeX

$$∀ z ∈ image₂ f s t, p z ⇔ ∀ a ∈ s, ∀ b ∈ t, p (f a b)$$

Lean4

theorem forall_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₂, forall_mem_image2]

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