α : Type u_3
β : Type ?u.35963
γ : Type ?u.35966
ι✝ : Sort ?u.35969
ι'✝ : Sort ?u.35972
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
inst✝ : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), HasBasis (l i) (p i) (s i)
h : Directed (fun x x_1 => x ≥ x_1) l
t : Set α
⊢ (t ∈ ⨅ (i : ι), l i) ↔ ∃ i, p i.fst i.snd ∧ s i.fst i.snd ⊆ t
α : Type u_3
β : Type ?u.35963
γ : Type ?u.35966
ι✝ : Sort ?u.35969
ι'✝ : Sort ?u.35972
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t : Set α
i : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
inst✝ : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), HasBasis (l i) (p i) (s i)
h : Directed (fun x x_1 => x ≥ x_1) l
⊢ HasBasis (⨅ (i : ι), l i) (fun ii' => p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd
refine' ⟨fun t => _⟩
α : Type u_3
β : Type ?u.35963
γ : Type ?u.35966
ι✝ : Sort ?u.35969
ι'✝ : Sort ?u.35972
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
inst✝ : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), HasBasis (l i) (p i) (s i)
h : Directed (fun x x_1 => x ≥ x_1) l
t : Set α
⊢ (∃ i, t ∈ l i) ↔ ∃ a b, p (a, b).fst (a, b).snd ∧ s (a, b).fst (a, b).snd ⊆ t
α : Type u_3
β : Type ?u.35963
γ : Type ?u.35966
ι✝ : Sort ?u.35969
ι'✝ : Sort ?u.35972
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
inst✝ : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), HasBasis (l i) (p i) (s i)
h : Directed (fun x x_1 => x ≥ x_1) l
t : Set α
⊢ (t ∈ ⨅ (i : ι), l i) ↔ ∃ i, p i.fst i.snd ∧ s i.fst i.snd ⊆ t
rw [mem_iInf_of_directed h, Prod.exists]
no goals
α : Type u_3
β : Type ?u.35963
γ : Type ?u.35966
ι✝ : Sort ?u.35969
ι'✝ : Sort ?u.35972
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Type u_1
ι' : Type u_2
inst✝ : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), HasBasis (l i) (p i) (s i)
h : Directed (fun x x_1 => x ≥ x_1) l
t : Set α
⊢ (∃ i, t ∈ l i) ↔ ∃ a b, p (a, b).fst (a, b).snd ∧ s (a, b).fst (a, b).snd ⊆ t
exact exists_congr fun i => (hl i).mem_iff