ball — Mathlib

English

A predicate holds for all elements of s(a,b) if and only if it holds for a and b.

Русский

Свойство P держится для всех элементов s(a,b) тогда и только тогда, когда оно держится для a и b.

LaTeX

$$$ \\forall {p:\\alpha \\to Prop},\\ {a,b:\\alpha},\\ Iff(\\forall c, c \\in s(a,b) \\to p(c)) (p(a) \\land p(b)). $$$

Lean4

theorem ball {p : α → Prop} {a b : α} : (∀ c ∈ s(a, b), p c) ↔ p a ∧ p b := by simp

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