English
Let A and B be families of Finset α. Then the r-sizedness of their union is equivalent to the conjunction of the r-sizedness of A and B: (A ∪ B).Sized r ↔ A.Sized r ∧ B.Sized r.
Русский
Пусть A и B являются семействами Finset α. Тогда r-размерность их объединения эквивалентна объединению размерности r каждого из A и B: (A ∪ B).Sized r ↔ A.Sized r ∧ B.Sized r.
LaTeX
$$$ (A \cup B).Sized r \iff A.Sized r \land B.Sized r $$$
Lean4
theorem sized_union : (A ∪ B).Sized r ↔ A.Sized r ∧ B.Sized r :=
⟨fun hA => ⟨hA.mono subset_union_left, hA.mono subset_union_right⟩, fun hA _x hx =>
hx.elim (fun h => hA.1 h) fun h => hA.2 h⟩
