α : Type u_1
β : Type ?u.900188
γ : Type ?u.900191
δ : Type ?u.900194
δ' : Type ?u.900197
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : Set α
⊢ IsMeasurablyGenerated (𝓟 s) → MeasurableSet s
α : Type u_1
β : Type ?u.900188
γ : Type ?u.900191
δ : Type ?u.900194
δ' : Type ?u.900197
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : Set α
⊢ IsMeasurablyGenerated (𝓟 s) ↔ MeasurableSet s
refine' ⟨_, fun hs => ⟨fun t ht => ⟨s, mem_principal_self s, hs, ht⟩⟩⟩
case mk
α : Type u_1
β : Type ?u.900188
γ : Type ?u.900191
δ : Type ?u.900194
δ' : Type ?u.900197
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t, t ∈ 𝓟 s ∧ MeasurableSet t ∧ t ⊆ s_1
⊢ MeasurableSet s
α : Type u_1
β : Type ?u.900188
γ : Type ?u.900191
δ : Type ?u.900194
δ' : Type ?u.900197
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : Set α
⊢ IsMeasurablyGenerated (𝓟 s) → MeasurableSet s
rintro ⟨hs⟩
case mk.intro.intro.intro
α : Type u_1
β : Type ?u.900188
γ : Type ?u.900191
δ : Type ?u.900194
δ' : Type ?u.900197
ι : Sort uι
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t, t ∈ 𝓟 s ∧ MeasurableSet t ∧ t ⊆ s_1
t : Set α
ht : t ∈ 𝓟 s
htm : MeasurableSet t
hts : t ⊆ s
⊢ MeasurableSet s
case mk
α : Type u_1
β : Type ?u.900188
γ : Type ?u.900191
δ : Type ?u.900194
δ' : Type ?u.900197
ι : Sort uι
s✝ t u : Set α
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t, t ∈ 𝓟 s ∧ MeasurableSet t ∧ t ⊆ s_1
⊢ MeasurableSet s
rcases hs (mem_principal_self s) with ⟨t, ht, htm, hts⟩
case mk.intro.intro.intro
α : Type u_1
β : Type ?u.900188
γ : Type ?u.900191
δ : Type ?u.900194
δ' : Type ?u.900197
ι : Sort uι
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t, t ∈ 𝓟 s ∧ MeasurableSet t ∧ t ⊆ s_1
t : Set α
ht : t ∈ 𝓟 s
htm : MeasurableSet t
hts : t ⊆ s
this : t = s
⊢ MeasurableSet s
case mk.intro.intro.intro
α : Type u_1
β : Type ?u.900188
γ : Type ?u.900191
δ : Type ?u.900194
δ' : Type ?u.900197
ι : Sort uι
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t, t ∈ 𝓟 s ∧ MeasurableSet t ∧ t ⊆ s_1
t : Set α
ht : t ∈ 𝓟 s
htm : MeasurableSet t
hts : t ⊆ s
⊢ MeasurableSet s
have : t = s := hts.antisymm ht
no goals
case mk.intro.intro.intro
α : Type u_1
β : Type ?u.900188
γ : Type ?u.900191
δ : Type ?u.900194
δ' : Type ?u.900197
ι : Sort uι
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
s : Set α
hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t, t ∈ 𝓟 s ∧ MeasurableSet t ∧ t ⊆ s_1
t : Set α
ht : t ∈ 𝓟 s
htm : MeasurableSet t
hts : t ⊆ s
this : t = s
⊢ MeasurableSet s
rwa [← this]