forall_mem_cons — Mathlib

English

For h : a ∉ s and predicate p, (∀ x, x ∈ cons a s h → p x) is equivalent to (p a ∧ ∀ x ∈ s, p x).

Русский

Для произвольного h: a ∉ s и предиката p верно: (для всех x, x ∈ cons a s h ⇒ p x) эквивалентно (p a ∧ ∀ x ∈ s, p x).

LaTeX

$$$(h : a \notin s) (p : \alpha \to Prop) : (\forall x, x \in\ cons\ a\ s\ h \to p\ x) \iff (p\ a) \land (\forall x, x \in s \to p\ x)$$$

Lean4

theorem forall_mem_cons (h : a ∉ s) (p : α → Prop) : (∀ x, x ∈ cons a s h → p x) ↔ p a ∧ ∀ x, x ∈ s → p x := by grind

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