gen_mono — Mathlib

English

UniformOnFun.gen is antitone in the first argument and monotone in the second: if S' ⊆ S and V ⊆ V', then UniformOnFun.gen 𝔖 S V ⊆ UniformOnFun.gen 𝔖 S' V'.

Русский

Генератор UniformOnFun является антитонным по первому аргументу и монотонным по второму: если S' ⊆ S и V ⊆ V', то UniformOnFun.gen 𝔖 S V ⊆ UniformOnFun.gen 𝔖 S' V'.

LaTeX

$$$\UniformOnFun.gen 𝔖 S V \subseteq UniformOnFun.gen 𝔖 S' V'\quad\text{whenever}\quad S' \subseteq S,\; V \subseteq V'.$$$

Lean4

/-- `UniformOnFun.gen` is antitone in the first argument and monotone in the second. -/
protected theorem gen_mono {𝔖} {S S' : Set α} {V V' : Set (β × β)} (hS : S' ⊆ S) (hV : V ⊆ V') :
    UniformOnFun.gen 𝔖 S V ⊆ UniformOnFun.gen 𝔖 S' V' := fun _uv h x hx => hV (h x <| hS hx)

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