antitone_bforall — Mathlib

English

Quantifying over a set is antitone in the set: if S ⊆ T, then ∀ x ∈ T, P x implies ∀ x ∈ S, P x.

Русский

Квантор по множеству антимонотонен по отношению к множеству: если S ⊆ T, то ∀ x ∈ T, P x ⇒ ∀ x ∈ S, P x.

LaTeX

$$$ S \subseteq T \Rightarrow (\forall x (x \in T \rightarrow P x)) \rightarrow (\forall x (x \in S \rightarrow P x)) $$$

Lean4

/-- Quantifying over a set is antitone in the set -/
theorem antitone_bforall {P : α → Prop} : Antitone fun s : Set α => ∀ x ∈ s, P x := fun _ _ hst h x hx => h x <| hst hx

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