ι : Type u_2
α : ι → Type u_1
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
⊢ s ∈ f i
ι : Type u_2
α : ι → Type u_1
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
⊢ map (eval i) (pi f) = f i
refine' le_antisymm (tendsto_eval_pi f i) fun s hs => _
case intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : Set.Finite I
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : Set.pi I t ⊆ eval i ⁻¹' s
⊢ s ∈ f i
ι : Type u_2
α : ι → Type u_1
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
⊢ s ∈ f i
rcases mem_pi.1 (mem_map.1 hs) with ⟨I, hIf, t, htf, hI⟩
case intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : Set.Finite I
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' Set.pi I t ⊆ s
⊢ s ∈ f i
case intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : Set.Finite I
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : Set.pi I t ⊆ eval i ⁻¹' s
⊢ s ∈ f i
rw [← image_subset_iff] at hI
case intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : Set.Finite I
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' Set.pi I t ⊆ s
⊢ Set.Nonempty (Set.pi I t)
case intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : Set.Finite I
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' Set.pi I t ⊆ s
⊢ s ∈ f i
refine' mem_of_superset (htf i) ((subset_eval_image_pi _ _).trans hI)
no goals
case intro.intro.intro.intro
ι : Type u_2
α : ι → Type u_1
f✝ f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), NeBot (f i)
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : Set.Finite I
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' Set.pi I t ⊆ s
⊢ Set.Nonempty (Set.pi I t)
exact nonempty_of_mem (pi_mem_pi hIf fun i _ => htf i)