finite_subset_iUnion — Mathlib

English

If s is finite and s ⊆ ⋃ i, t i, then there exists a finite I such that s ⊆ ⋃ i ∈ I, t i.

Русский

Если s конечно и s ⊆ ⋃ i, t i, то существует конечный подмножество индексов I, такое что s ⊆ ⋃ i ∈ I, t i.

LaTeX

$$$\\exists I, I\\ Finite \\land s \\subseteq \\bigcup_{i \\in I} t(i)$$$

Lean4

theorem finite_subset_iUnion {s : Set α} (hs : s.Finite) {ι} {t : ι → Set α} (h : s ⊆ ⋃ i, t i) :
    ∃ I : Set ι, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i := by
  have := hs.to_subtype
  choose f hf using show ∀ x : s, ∃ i, x.1 ∈ t i by simpa [subset_def] using h
  refine ⟨range f, finite_range f, fun x hx => ?_⟩
  rw [biUnion_range, mem_iUnion]
  exact ⟨⟨x, hx⟩, hf _⟩

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