forall_sups_iff — Mathlib

English

For any predicate p, p holds for all elements of s ⊻ t iff p holds for all a ∈ s and all b ∈ t on a ⊔ b.

Русский

Для любого предиката p выполнение p на всех элементах s ⊻ t эквивалентно выполнению p на каждом a ⊔ b с a ∈ s, b ∈ t.

LaTeX

$$$ \forall p:\mathrm{α} \to \mathrm{Prop},\ ( \forall c \in s \ ⊻ \ t,\ p(c) ) \iff ( \forall a \in s,\ \forall b \in t,\ p(a \⊔ b) )$$$

Lean4

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

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