monotone_dom — Mathlib

English

The map sending a partial equivalence to its domain is monotone with respect to the order on partial equivalences.

Русский

Отображение частичной эквивалентности в её область монотонно по отношению к порядку частичных эквивалентностей.

LaTeX

$$$\text{Monotone}(\lambda f : M \equiv_p^L N, f.\mathrm{dom}).$$$

Lean4

theorem monotone_dom : Monotone (fun f : M ≃ₚ[L] N ↦ f.dom) := fun _ _ ↦ dom_le_dom

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