monotone_cod

Mathlib.ModelTheory.PartialEquiv

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.PartialEquiv.monotone_cod

English

The map sending a partial equivalence to its codomain is monotone.

Русский

Отображение частичной эквивалентности в её кодомонотонно.

LaTeX

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

Lean4

theorem monotone_cod : Monotone (fun f : M ≃ₚ[L] N ↦ f.cod) := fun _ _ ↦ cod_le_cod

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru