English
If the union of a family s of sets is unbounded and the index family is smaller than cof(swap rᶜ), then some member of the family is unbounded.
Русский
Если объединение семейства множеств несобираемо и размер множества индексов меньше cof(swap rᶜ), то существует элемент этого семейства, который неограничен.
LaTeX
$$$$ \text{If } \operatorname{Unbounded}(r, \bigcup s) \text{ and } |s| < \operatorname{cof}(\mathrm{swap}(r^c)), \text{ then } \exists x \in s, \ \operatorname{Unbounded}(r, x). $$$$
Lean4
/-- If the union of s is unbounded and s is smaller than the cofinality,
then s has an unbounded member -/
theorem unbounded_of_unbounded_sUnion (r : α → α → Prop) [wo : IsWellOrder α r] {s : Set (Set α)}
(h₁ : Unbounded r <| ⋃₀ s) (h₂ : #s < Order.cof (swap rᶜ)) : ∃ x ∈ s, Unbounded r x :=
by
by_contra! h
simp_rw [not_unbounded_iff] at h
let f : s → α := fun x : s => wo.wf.sup x (h x.1 x.2)
refine h₂.not_ge (le_trans (csInf_le' ⟨range f, fun x => ?_, rfl⟩) mk_range_le)
rcases h₁ x with ⟨y, ⟨c, hc, hy⟩, hxy⟩
exact ⟨f ⟨c, hc⟩, mem_range_self _, fun hxz => hxy (Trans.trans (wo.wf.lt_sup _ hy) hxz)⟩
