forall_mem_diffs — Mathlib

English

For any p : α → Prop, (∀ c ∈ s \\ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a \\ b).

Русский

Для любого p: α → Prop выполняется эквивалентно: (∀ c ∈ s \\ t, p c) эквивалентно (∀ a ∈ s, ∀ b ∈ t, p (a \\ b)).

LaTeX

$$$ (\\forall c \\in s \\\\ t, p c) \\iff (\\forall a \\in s, \\forall b \\in t, p (a \\\\ b)) $$$

Lean4

theorem forall_mem_diffs {p : α → Prop} : (∀ c ∈ s \\ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a \ b) :=
  forall_mem_image₂

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