antitone_setOf — Mathlib

English

If for every b the predicate a ↦ p(a,b) is antitone, then a ↦ { b | p(a,b) } is antitone.

Русский

Если для каждого b предикат a ↦ p(a,b) антимонтона, то a ↦ { b | p(a,b) } антимонотна.

LaTeX

$$$ [\text{Preorder } \alpha] \ {p : \alpha \to \beta \to \text{Prop}} (hp : \forall b, \operatorname{Antitone}(a \mapsto p(a,b))) : \operatorname{Antitone}(a \mapsto \{ b \mid p(a,b) \})$$$

Lean4

theorem antitone_setOf [Preorder α] {p : α → β → Prop} (hp : ∀ b, Antitone fun a => p a b) :
    Antitone fun a => {b | p a b} := fun _ _ h b => hp b h

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