forall_mem_compls — Mathlib

English

For any predicate p, ∀ a ∈ sᶜˢ, p a holds iff ∀ a ∈ s, p(aᶜ) holds.

Русский

Для любого предиката p, ∀a ∈ sᶜˢ, p(a) справедливо тогда и только тогда, когда ∀a ∈ s, p(aᶜ) справедливо.

LaTeX

$$$ (\\forall a \\in s^{\\complement\\}\\!ˢ) p(a) \\iff (\\forall a \\in s) p(a^{\\complement}) $$$

Lean4

theorem forall_mem_compls {p : α → Prop} : (∀ a ∈ sᶜˢ, p a) ↔ ∀ a ∈ s, p aᶜ :=
  forall_mem_map

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