monotone_setOf — Mathlib

English

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

Русский

Если для каждого 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{Monotone}(a \mapsto p(a,b))) : \operatorname{Monotone}(a \mapsto \{ b \mid p(a,b) \})$$$

Lean4

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

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