nonempty_left

Mathlib.GroupTheory.Complement

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

English

If IsComplement S T then S is nonempty.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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