α : Type u_1
C : Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : C ∅
h_basic : ∀ (t : Set α), t ∈ s → C t
h_compl : ∀ (t : Set α), MeasurableSet t → C t → C (tᶜ)
h_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)
⊢ MeasurableSet = DynkinSystem.GenerateHas s
α : Type u_1
C : Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : C ∅
h_basic : ∀ (t : Set α), t ∈ s → C t
h_compl : ∀ (t : Set α), MeasurableSet t → C t → C (tᶜ)
h_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)
⊢ MeasurableSet = DynkinSystem.GenerateHas s
rw [h_eq, DynkinSystem.generateFrom_eq h_inter]
no goals
α : Type u_1
C : Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : C ∅
h_basic : ∀ (t : Set α), t ∈ s → C t
h_compl : ∀ (t : Set α), MeasurableSet t → C t → C (tᶜ)
h_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)
⊢ MeasurableSet = DynkinSystem.GenerateHas s
rfl
no goals
α : Type u_1
C : Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : C ∅
h_basic : ∀ (t : Set α), t ∈ s → C t
h_compl : ∀ (t : Set α), MeasurableSet t → C t → C (tᶜ)
h_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)
eq : MeasurableSet = DynkinSystem.GenerateHas s
t : Set α
ht : MeasurableSet t
⊢ DynkinSystem.GenerateHas s t
rwa [eq] at ht
α : Type u_1
C : Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : C ∅
h_basic : ∀ (t : Set α), t ∈ s → C t
h_compl : ∀ (t : Set α), MeasurableSet t → C t → C (tᶜ)
h_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)
eq : MeasurableSet = DynkinSystem.GenerateHas s
t✝ : Set α
ht✝ : MeasurableSet t✝
this : DynkinSystem.GenerateHas s t✝
t : Set α
ht : DynkinSystem.GenerateHas s t
⊢ DynkinSystem.GenerateHas s t
α : Type u_1
C : Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : C ∅
h_basic : ∀ (t : Set α), t ∈ s → C t
h_compl : ∀ (t : Set α), MeasurableSet t → C t → C (tᶜ)
h_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)
eq : MeasurableSet = DynkinSystem.GenerateHas s
t✝ : Set α
ht✝ : MeasurableSet t✝
this : DynkinSystem.GenerateHas s t✝
t : Set α
ht : DynkinSystem.GenerateHas s t
⊢ MeasurableSet t
rw [eq]
no goals
α : Type u_1
C : Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : C ∅
h_basic : ∀ (t : Set α), t ∈ s → C t
h_compl : ∀ (t : Set α), MeasurableSet t → C t → C (tᶜ)
h_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)
eq : MeasurableSet = DynkinSystem.GenerateHas s
t✝ : Set α
ht✝ : MeasurableSet t✝
this : DynkinSystem.GenerateHas s t✝
t : Set α
ht : DynkinSystem.GenerateHas s t
⊢ DynkinSystem.GenerateHas s t
exact ht
α : Type u_1
C : Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : C ∅
h_basic : ∀ (t : Set α), t ∈ s → C t
h_compl : ∀ (t : Set α), MeasurableSet t → C t → C (tᶜ)
h_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)
eq : MeasurableSet = DynkinSystem.GenerateHas s
t : Set α
ht✝ : MeasurableSet t
this : DynkinSystem.GenerateHas s t
f : ℕ → Set α
hf : Pairwise (Disjoint on f)
ht : ∀ (i : ℕ), DynkinSystem.GenerateHas s (f i)
i : ℕ
⊢ DynkinSystem.GenerateHas s (f i)
α : Type u_1
C : Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : C ∅
h_basic : ∀ (t : Set α), t ∈ s → C t
h_compl : ∀ (t : Set α), MeasurableSet t → C t → C (tᶜ)
h_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)
eq : MeasurableSet = DynkinSystem.GenerateHas s
t : Set α
ht✝ : MeasurableSet t
this : DynkinSystem.GenerateHas s t
f : ℕ → Set α
hf : Pairwise (Disjoint on f)
ht : ∀ (i : ℕ), DynkinSystem.GenerateHas s (f i)
i : ℕ
⊢ MeasurableSet (f i)
rw [eq]
no goals
α : Type u_1
C : Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : C ∅
h_basic : ∀ (t : Set α), t ∈ s → C t
h_compl : ∀ (t : Set α), MeasurableSet t → C t → C (tᶜ)
h_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)
eq : MeasurableSet = DynkinSystem.GenerateHas s
t : Set α
ht✝ : MeasurableSet t
this : DynkinSystem.GenerateHas s t
f : ℕ → Set α
hf : Pairwise (Disjoint on f)
ht : ∀ (i : ℕ), DynkinSystem.GenerateHas s (f i)
i : ℕ
⊢ DynkinSystem.GenerateHas s (f i)
exact ht _