filter_ne_average_add_one_eq_average

English

The set of parts with size not equal to average plus one is exactly the set of parts with size equal to the average.

Русский

Множество частей с размером, не равным среднему, плюс 1, равно множеству частей с размером, равным среднему.

LaTeX

$${p ∈ P.parts | ¬|p| = |s|/|P.parts| + 1} = {p ∈ P.parts | |p| = |s|/|P.parts|}$$

Lean4

theorem filter_ne_average_add_one_eq_average (hP : P.IsEquipartition) :
    {p ∈ P.parts | ¬#p = #s / #P.parts + 1} = {p ∈ P.parts | #p = #s / #P.parts} :=
  by
  ext p
  simp only [mem_filter, and_congr_right_iff]
  exact fun hp ↦ (hP.card_part_eq_average_iff hp).symm

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