self_subset_generateMeasurableRec

English

Every element of s is contained in generateMeasurableRec s i.

Русский

Каждый элемент множества s содержится в generateMeasurableRec s i.

LaTeX

$$$\\forall (t \\in s), t \\subseteq \\mathrm{generateMeasurableRec}(s,i)$$$

Lean4

theorem self_subset_generateMeasurableRec (s : Set (Set α)) (i : Ordinal) : s ⊆ generateMeasurableRec s i :=
  by
  unfold generateMeasurableRec
  apply_rules [subset_union_of_subset_left]
  exact subset_rfl

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