mono_coe

Mathlib.Order.Monotone.Defs

URI: https://scilib.ai/kg/mathlib#Subtype.mono_coe

English

The inclusion map from a subtype to the ambient type is monotone.

Русский

Включение подмножества в исходный тип тождественно монотонно.

LaTeX

$$$\forall x,y,\ x\le y \Rightarrow x\le y$ на Subtype.$$

Lean4

theorem mono_coe [Preorder α] (t : Set α) : Monotone ((↑) : Subtype t → α) := fun _ _ ↦ id

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

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

Разделы

Аффилиация

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