card_le_m_add_one_of_mem_chunk_parts

Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

URI: https://scilib.ai/kg/mathlib#SzemerediRegularity.card_le_m_add_one_of_mem_chunk_parts

← MathLib Explorer

English

If s ∈ (chunk hP G ε hU).parts then s.card is either ⌊...⌋ or ⌈...⌉ around m.

Русский

Если s ∈ (chunk...).parts, то cardinality s.card близка к m, то есть равна ⌊m⌋ или ⌈m⌉.

LaTeX

$$s.card ∈ {m, m+1}$$

Lean4

theorem card_le_m_add_one_of_mem_chunk_parts (hs : s ∈ (chunk hP G ε hU).parts) : #s ≤ m + 1 :=
  (card_eq_of_mem_parts_chunk hs).elim (fun i => by simp [i]) fun i => i.le

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

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

Разделы

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

Аффилиация

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