nonempty_right

Mathlib.GroupTheory.Complement

URI: https://scilib.ai/kg/mathlib#Subgroup.IsComplement.nonempty_right

English

If IsComplement S T then T is nonempty.

Русский

Если S и T образуют дополнение, то T непусто.

LaTeX

$$$ \text{IsComplement } S T \Rightarrow T \neq \varnothing$.$$

Lean4

@[to_additive]
theorem nonempty_right (hst : IsComplement S T) : T.Nonempty := by contrapose! hst; simp [hst]

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

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

Разделы

Аффилиация

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