case a
α : Type u_1
β : Type ?u.14406
γ : Type ?u.14409
ι : Sort u_2
ι' : Sort ?u.14415
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : HasBasis l p s
U : Set α
⊢ U ∈ IsBasis.filter (_ : IsBasis p s) ↔ U ∈ l
α : Type u_1
β : Type ?u.14406
γ : Type ?u.14409
ι : Sort u_2
ι' : Sort ?u.14415
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : HasBasis l p s
⊢ IsBasis.filter (_ : IsBasis p s) = l
ext U
no goals
case a
α : Type u_1
β : Type ?u.14406
γ : Type ?u.14409
ι : Sort u_2
ι' : Sort ?u.14415
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : HasBasis l p s
U : Set α
⊢ U ∈ IsBasis.filter (_ : IsBasis p s) ↔ U ∈ l
simp [h.mem_iff, IsBasis.mem_filter_iff]