case a
α : Type u_1
β : Type ?u.8511
γ : Type ?u.8514
ι : Sort ?u.8517
ι' : Sort ?u.8520
B : FilterBasis α
⊢ generate B.sets ≤ FilterBasis.filter B

case a
α : Type u_1
β : Type ?u.8511
γ : Type ?u.8514
ι : Sort ?u.8517
ι' : Sort ?u.8520
B : FilterBasis α
⊢ FilterBasis.filter B ≤ generate B.sets
α : Type u_1
β : Type ?u.8511
γ : Type ?u.8514
ι : Sort ?u.8517
ι' : Sort ?u.8520
B : FilterBasis α
⊢ generate B.sets = FilterBasis.filter B
apply le_antisymm
case a
α : Type u_1
β : Type ?u.8511
γ : Type ?u.8514
ι : Sort ?u.8517
ι' : Sort ?u.8520
B : FilterBasis α
U : Set α
U_in : U ∈ FilterBasis.filter B
⊢ U ∈ generate B.sets
case a
α : Type u_1
β : Type ?u.8511
γ : Type ?u.8514
ι : Sort ?u.8517
ι' : Sort ?u.8520
B : FilterBasis α
⊢ generate B.sets ≤ FilterBasis.filter B
intro U U_in
case a.intro.intro
α : Type u_1
β : Type ?u.8511
γ : Type ?u.8514
ι : Sort ?u.8517
ι' : Sort ?u.8520
B : FilterBasis α
U : Set α
U_in : U ∈ FilterBasis.filter B
V : Set α
V_in : V ∈ B
h : V ⊆ U
⊢ U ∈ generate B.sets
case a
α : Type u_1
β : Type ?u.8511
γ : Type ?u.8514
ι : Sort ?u.8517
ι' : Sort ?u.8520
B : FilterBasis α
U : Set α
U_in : U ∈ FilterBasis.filter B
⊢ U ∈ generate B.sets
rcases B.mem_filter_iff.mp U_in with ⟨V, V_in, h⟩
no goals
case a.intro.intro
α : Type u_1
β : Type ?u.8511
γ : Type ?u.8514
ι : Sort ?u.8517
ι' : Sort ?u.8520
B : FilterBasis α
U : Set α
U_in : U ∈ FilterBasis.filter B
V : Set α
V_in : V ∈ B
h : V ⊆ U
⊢ U ∈ generate B.sets
exact GenerateSets.superset (GenerateSets.basic V_in) h
case a
α : Type u_1
β : Type ?u.8511
γ : Type ?u.8514
ι : Sort ?u.8517
ι' : Sort ?u.8520
B : FilterBasis α
⊢ B.sets ⊆ (FilterBasis.filter B).sets
case a
α : Type u_1
β : Type ?u.8511
γ : Type ?u.8514
ι : Sort ?u.8517
ι' : Sort ?u.8520
B : FilterBasis α
⊢ FilterBasis.filter B ≤ generate B.sets
rw [le_generate_iff]
no goals
case a
α : Type u_1
β : Type ?u.8511
γ : Type ?u.8514
ι : Sort ?u.8517
ι' : Sort ?u.8520
B : FilterBasis α
⊢ B.sets ⊆ (FilterBasis.filter B).sets
apply mem_filter_of_mem