case base
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t s : Set α
h_s : s ∈ S
⊢ s ∈ generatePiSystem T

case inter
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t s u : Set α
h_s✝ : generatePiSystem S s
h_t✝ : generatePiSystem S u
h_nonempty : Set.Nonempty (s ∩ u)
h_s : s ∈ generatePiSystem T
h_u : u ∈ generatePiSystem T
⊢ s ∩ u ∈ generatePiSystem T
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t : Set α
ht : t ∈ generatePiSystem S
⊢ t ∈ generatePiSystem T
induction' ht with s h_s s u _ _ h_nonempty h_s h_u
no goals
case base
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t s : Set α
h_s : s ∈ S
⊢ s ∈ generatePiSystem T
exact generatePiSystem.base (Set.mem_of_subset_of_mem hST h_s)
no goals
case inter
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t s u : Set α
h_s✝ : generatePiSystem S s
h_t✝ : generatePiSystem S u
h_nonempty : Set.Nonempty (s ∩ u)
h_s : s ∈ generatePiSystem T
h_u : u ∈ generatePiSystem T
⊢ s ∩ u ∈ generatePiSystem T
exact isPiSystem_generatePiSystem T _ h_s _ h_u h_nonempty