unbounded_of_unbounded_iUnion — Mathlib

English

If the union over i of s(i) is unbounded and cof less than cof(...), then there exists x such that Unbounded r (s x).

Русский

Если объединение по i семейства s(i) неограничено и cof достаточно большое, существует индекс x, для которого s(x) неограничено по r.

LaTeX

$$$$ \exists x:\beta,\ Unbounded(r, s(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_iUnion {α β : Type u} (r : α → α → Prop) [wo : IsWellOrder α r] (s : β → Set α)
    (h₁ : Unbounded r <| ⋃ x, s x) (h₂ : #β < Order.cof (swap rᶜ)) : ∃ x : β, Unbounded r (s x) :=
  by
  rw [← sUnion_range] at h₁
  rcases unbounded_of_unbounded_sUnion r h₁ (mk_range_le.trans_lt h₂) with ⟨_, ⟨x, rfl⟩, u⟩
  exact ⟨x, u⟩

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