English
Equivalence between the range and smaller via a bijection.
Русский
Эквивалентность диапазона и меньшего через биекция.
LaTeX
$$$$\\text{Equiv}\\; (\\mathrm{range}\\; (\\mathrm{π}\\ C)) \\; (\\mathrm{smaller}) $$$$
Lean4
theorem limitOrdinal (l : Products I) :
l.isGood (π C (ord I · < o)) ↔ ∃ (o' : Ordinal), o' < o ∧ l.isGood (π C (ord I · < o')) :=
by
refine ⟨fun h ↦ ?_, fun ⟨o', ⟨ho', hl⟩⟩ ↦ isGood_mono C (le_of_lt ho') hl⟩
use Finset.sup l.val.toFinset (fun a ↦ Order.succ (ord I a))
have hslt : Finset.sup l.val.toFinset (fun a ↦ Order.succ (ord I a)) < o :=
by
simp only [Finset.sup_lt_iff ho.bot_lt, List.mem_toFinset]
exact fun b hb ↦ ho.succ_lt (prop_of_isGood C (ord I · < o) h b hb)
refine ⟨hslt, fun he ↦ h ?_⟩
have hlt : ∀ i ∈ l.val, ord I i < Finset.sup l.val.toFinset (fun a ↦ Order.succ (ord I a)) :=
by
intro i hi
simp only [Finset.lt_sup_iff, List.mem_toFinset, Order.lt_succ_iff]
exact ⟨i, hi, le_rfl⟩
rwa [eval_πs_image' C (le_of_lt hslt) hlt, ← eval_πs' C (le_of_lt hslt) hlt,
Submodule.apply_mem_span_image_iff_mem_span (injective_πs' C _)]
