dom_le_dom

Mathlib.ModelTheory.PartialEquiv

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

English

If f ≤ g for partial equivalences, then f.dom ≤ g.dom.

Русский

Если f ≤ g для частичных эквивалентов, то область определения f лежит в области определения g.

LaTeX

$$$ f \le g \Rightarrow f.\mathrm{dom} \le g.\mathrm{dom} $$$

Lean4

@[gcongr]
theorem dom_le_dom {f g : M ≃ₚ[L] N} : f ≤ g → f.dom ≤ g.dom := fun ⟨le, _⟩ ↦ le

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

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

Разделы

Аффилиация

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