small_union — Mathlib

English

If s and t are small subsets of α, then their union s ∪ t is small.

Русский

Если s и t — малые подмножественные α, то их объединение s ∪ t — тоже малое.

LaTeX

$$$\operatorname{Small}(s) \land \operatorname{Small}(t) \Rightarrow \operatorname{Small}(s \cup t)$$$

Lean4

instance small_union (s t : Set α) [Small.{u} s] [Small.{u} t] : Small.{u} (s ∪ t : Set α) :=
  by
  rw [← Subtype.range_val (s := s), ← Subtype.range_val (s := t), ← Set.Sum.elim_range]
  infer_instance

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