English
For any families f,g: ι → Cardinal with f(i) < g(i) for all i, the sum of f is strictly less than the product of g: sum f < prod g.
Русский
Для любых семей f,g: ι → Cardinal с условием f(i) < g(i) для всех i имеет место неравенство sum f < prod g.
LaTeX
$$∀ f,g, (∀ i, f(i) < g(i)) → sum f < prod g$$
Lean4
/-- **König's theorem** -/
theorem sum_lt_prod {ι} (f g : ι → Cardinal) (H : ∀ i, f i < g i) : sum f < prod g :=
lt_of_not_ge fun ⟨F⟩ =>
by
have : Inhabited (∀ i : ι, (g i).out) :=
by
refine ⟨fun i => Classical.choice <| mk_ne_zero_iff.1 ?_⟩
rw [mk_out]
exact (H i).ne_bot
let G := invFun F
have sG : Surjective G := invFun_surjective F.2
choose C hc using
show ∀ i, ∃ b, ∀ a, G ⟨i, a⟩ i ≠ b by
intro i
simp only [not_exists.symm, not_forall.symm]
refine fun h => (H i).not_ge ?_
rw [← mk_out (f i), ← mk_out (g i)]
exact ⟨Embedding.ofSurjective _ h⟩
let ⟨⟨i, a⟩, h⟩ := sG C
exact hc i a (congr_fun h _)
