forall_mem_pair — Mathlib

English

For any P: α → Prop and a,b ∈ α, (∀ x ∈ s(a,b), P x) ↔ P a ∧ P b.

Русский

Для любого P: α → Prop и любых a,b ∈ α, (∀ x ∈ s(a,b), P x) эквивалентно P a ∧ P b.

LaTeX

$$$ \\forall {P : \\alpha \\to Prop} {a b : \\alpha}, (\\forall x \\in s(a,b), P x) \\iff P a \\land P b. $$$

Lean4

theorem forall_mem_pair {P : α → Prop} {a b : α} : (∀ x ∈ s(a, b), P x) ↔ P a ∧ P b := by
  simp only [mem_iff, forall_eq_or_imp, forall_eq]

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