map_le_range

Mathlib.ModelTheory.Substructures

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Hom.map_le_range

English

If closure L s = ⊤ and f,g coincide on s, then f = g.

Русский

Если замыкание L s равно верхнему, и f и g совпадают на s, то f = g.

LaTeX

$$$ \operatorname{closure}_L(s) = \top \Rightarrow \bigl(\text{EqOn}(f,g,s) \Rightarrow f=g\bigr) $$$

Lean4

theorem map_le_range {f : M →[L] N} {p : L.Substructure M} : map f p ≤ range f :=
  SetLike.coe_mono (Set.image_subset_range f p)

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

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

Разделы

Аффилиация

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