empty_mem_generateMeasurableRec — Mathlib

English

The empty set belongs to generateMeasurableRec s i for any i.

Русский

Пустое множество принадлежит generateMeasurableRec s i для любого i.

LaTeX

$$$\\emptyset \\in generateMeasurableRec(s,i)$$$

Lean4

theorem empty_mem_generateMeasurableRec (s : Set (Set α)) (i : Ordinal) : ∅ ∈ generateMeasurableRec s i :=
  by
  unfold generateMeasurableRec
  exact mem_union_left _ (mem_union_left _ (mem_union_right _ (mem_singleton ∅)))

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