range_coe

Mathlib.Order.CompleteSublattice

URI: https://scilib.ai/kg/mathlib#CompleteLatticeHom.range_coe

English

If f: α → β is a complete lattice homomorphism and injective, then α is order-isomorphic to its range f(α).

Русский

Пусть f: α → β — гомоморфизм полной решетки и инъективен; тогда α изоморфна по порядку своему диапазону f(α).

LaTeX

$$$\operatorname{Injective}(f) \Rightarrow \alpha \cong_o f(\alpha)$$$

Lean4

theorem range_coe : (f.range : Set β) = range f :=
  rfl

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

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

Разделы

Аффилиация

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