instPartialOrderOpenSubgroup

Mathlib.Topology.Algebra.OpenSubgroup

URI: https://scilib.ai/kg/mathlib#OpenSubgroup.instPartialOrderOpenSubgroup

English

OpenSubgroup G forms a partially ordered set under inclusion.

Русский

OpenSubgroup G образует частично упорядоченное множество по включению.

LaTeX

$$$$ \\text{OpenSubgroup}(G) \\text{ is a partially ordered set with } U \\le V \\iff U \\subseteq V. $$$$

Lean4

@[to_additive]
instance instPartialOrderOpenSubgroup : PartialOrder (OpenSubgroup G) :=
  inferInstance

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

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

Разделы

Аффилиация

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