α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ ∅ ∈
    let i := i;
    let S := ⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j;
    s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ (n : ℕ), ↑(f n)
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ ∅ ∈ generateMeasurableRec s i
unfold generateMeasurableRec
no goals
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ ∅ ∈
    let i := i;
    let S := ⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j;
    s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ (n : ℕ), ↑(f n)
exact mem_union_left _ (mem_union_left _ (mem_union_right _ (mem_singleton ∅)))