forall_sups_iff — Mathlib

English

A property p holds for all sums iff it holds for all pairwise sums a ⊔ b with a ∈ s and b ∈ t.

Русский

Свойство p выполняется для всех сумм тогда и только тогда, когда оно выполняется для всех парных сумм a ⊔ b с a ∈ s и b ∈ t.

LaTeX

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

Lean4

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

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