one_le

Mathlib.Combinatorics.Additive.ApproximateSubgroup

URI: https://scilib.ai/kg/mathlib#IsApproximateSubgroup.one_le

← MathLib Explorer

English

If A is a K-approximate subgroup, then 1 ≤ K.

Русский

Если A является K-приближённой подпгруппой, то 1 ≤ K.

LaTeX

$$$1 \\le K$$$

Lean4

@[to_additive one_le]
theorem one_le (hA : IsApproximateSubgroup K A) : 1 ≤ K :=
  by
  obtain ⟨F, hF, hSF⟩ := hA.sq_covBySMul
  have hF₀ : F ≠ ∅ := by rintro rfl; simp [hA.nonempty.pow.ne_empty] at hSF
  exact hF.trans' <| by simpa [Finset.nonempty_iff_ne_empty]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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