strictMono_setCongr — Mathlib

English

If S = T for subsets of α with a preorder, then the induced map setCongr(h) is strictly monotone.

Русский

Если S = T для подмножеств α в предикаторном окружении, то соответствующее отображение setCongr(h) строго монотонно.

LaTeX

$$$\operatorname{StrictMono}(\mathrm{setCongr}(h))$ for $h:S=T$ with $[\text{Preorder } \alpha]$.$$

Lean4

theorem strictMono_setCongr {α : Type*} [Preorder α] {S T : Set α} (h : S = T) : StrictMono (setCongr h) := fun _ _ ↦ id

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