English
Let a ⊆ ι be infinite and s : ι → Set α satisfy that s is injective on a (i.e., s is injective when restricted to a). Then the union ⋃_{i∈a} s(i) is infinite.
Русский
Пусть a ⊆ ι бесконечно и функция s : ι → Set α такова, что она инъективна на a (то есть инъективна при ограничении до a). Тогда объединение ⋃_{i∈a} s(i) бесконечно.
LaTeX
$$$a \text{ бесконечно},\; s\text{ на } a\text{ инъективна} \Rightarrow (\bigcup_{i \in a} s(i)) \text{ бесконечно}.$$$
Lean4
theorem biUnion {ι : Type*} {s : ι → Set α} {a : Set ι} (ha : a.Infinite) (hs : a.InjOn s) : (⋃ i ∈ a, s i).Infinite :=
by
rw [biUnion_eq_iUnion]
have _ := ha.to_subtype
exact infinite_iUnion fun ⟨i, hi⟩ ⟨j, hj⟩ hij ↦ by simp [hs hi hj hij]
