α : Type u
β : Type v
γ : Type w
δ : Type ?u.96376
ι : Sort x
f✝ g : Filter α
s✝ t✝ : Set α
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) s
ne : Set.Nonempty s
t : Set α
this : Nonempty ↑s
⊢ (t ∈ ⨅ (i : β) (_ : i ∈ s), f i) ↔ ∃ i, i ∈ s ∧ t ∈ f i
α : Type u
β : Type v
γ : Type w
δ : Type ?u.96376
ι : Sort x
f✝ g : Filter α
s✝ t✝ : Set α
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) s
ne : Set.Nonempty s
t : Set α
⊢ (t ∈ ⨅ (i : β) (_ : i ∈ s), f i) ↔ ∃ i, i ∈ s ∧ t ∈ f i
haveI := ne.to_subtype
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.96376
ι : Sort x
f✝ g : Filter α
s✝ t✝ : Set α
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) s
ne : Set.Nonempty s
t : Set α
this : Nonempty ↑s
⊢ (t ∈ ⨅ (i : β) (_ : i ∈ s), f i) ↔ ∃ i, i ∈ s ∧ t ∈ f i
simp_rw [iInf_subtype', mem_iInf_of_directed h.directed_val, Subtype.exists, exists_prop]