case base
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x s✝ : Set α
h_s : s✝ ∈ S
⊢ s✝ ∈ S

case inter
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x s u : Set α
h_s✝ : generatePiSystem S s
h_t✝ : generatePiSystem S u
h_nonempty : Set.Nonempty (s ∩ u)
h_s : s ∈ S
h_u : u ∈ S
⊢ s ∩ u ∈ S
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x : Set α
h : x ∈ generatePiSystem S
⊢ x ∈ S
induction' h with _ h_s s u _ _ h_nonempty h_s h_u
no goals
case base
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x s✝ : Set α
h_s : s✝ ∈ S
⊢ s✝ ∈ S
exact h_s
no goals
case inter
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x s u : Set α
h_s✝ : generatePiSystem S s
h_t✝ : generatePiSystem S u
h_nonempty : Set.Nonempty (s ∩ u)
h_s : s ∈ S
h_u : u ∈ S
⊢ s ∩ u ∈ S
exact h_S _ h_s _ h_u h_nonempty