α : Type u_2
β : Type u_3
γ : Type ?u.23378
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
⊢ s ∈ Filter.lift (iInf f) g → s ∈ ⨅ (i : ι), Filter.lift (f i) g
α : Type u_2
β : Type u_3
γ : Type ?u.23378
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
⊢ Filter.lift (iInf f) g = ⨅ (i : ι), Filter.lift (f i) g
refine' lift_iInf_le.antisymm fun s => _
α : Type u_2
β : Type u_3
γ : Type ?u.23378
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
H : ∀ (t : Set α), t ∈ iInf f → (⨅ (i : ι), Filter.lift (f i) g) ≤ g t
⊢ ∀ (x : Set α), x ∈ iInf f → s ∈ g x → s ∈ ⨅ (i : ι), Filter.lift (f i) g
α : Type u_2
β : Type u_3
γ : Type ?u.23378
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
H : ∀ (t : Set α), t ∈ iInf f → (⨅ (i : ι), Filter.lift (f i) g) ≤ g t
⊢ s ∈ Filter.lift (iInf f) g → s ∈ ⨅ (i : ι), Filter.lift (f i) g
simp only [mem_lift_sets (Monotone.of_map_inf hg), exists_imp, and_imp]
no goals
α : Type u_2
β : Type u_3
γ : Type ?u.23378
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
H : ∀ (t : Set α), t ∈ iInf f → (⨅ (i : ι), Filter.lift (f i) g) ≤ g t
⊢ ∀ (x : Set α), x ∈ iInf f → s ∈ g x → s ∈ ⨅ (i : ι), Filter.lift (f i) g
exact fun t ht hs => H t ht hs
α : Type u_2
β : Type u_3
γ : Type ?u.23378
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
⊢ (⨅ (i : ι), Filter.lift (f i) g) ≤ g t
α : Type u_2
β : Type u_3
γ : Type ?u.23378
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
⊢ ∀ (t : Set α), t ∈ iInf f → (⨅ (i : ι), Filter.lift (f i) g) ≤ g t
intro t ht
case refine'_1
α : Type u_2
β : Type u_3
γ : Type ?u.23378
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
⊢ (⨅ (i : ι), Filter.lift (f i) g) ≤ g univ

case refine'_2
α : Type u_2
β : Type u_3
γ : Type ?u.23378
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht✝ : t ∈ iInf f
i✝ : ι
s₁✝ s₂✝ : Set α
hs : s₁✝ ∈ f i✝
ht : (⨅ (i : ι), Filter.lift (f i) g) ≤ g s₂✝
⊢ (⨅ (i : ι), Filter.lift (f i) g) ≤ g (s₁✝ ∩ s₂✝)
α : Type u_2
β : Type u_3
γ : Type ?u.23378
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
⊢ (⨅ (i : ι), Filter.lift (f i) g) ≤ g t
refine' iInf_sets_induct ht _ fun hs ht => _
case refine'_1
α : Type u_2
β : Type u_3
γ : Type ?u.23378
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
inhabited_h : Inhabited ι
⊢ (⨅ (i : ι), Filter.lift (f i) g) ≤ g univ
case refine'_1
α : Type u_2
β : Type u_3
γ : Type ?u.23378
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
⊢ (⨅ (i : ι), Filter.lift (f i) g) ≤ g univ
inhabit ι
no goals
case refine'_1
α : Type u_2
β : Type u_3
γ : Type ?u.23378
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
inhabited_h : Inhabited ι
⊢ (⨅ (i : ι), Filter.lift (f i) g) ≤ g univ
exact iInf₂_le_of_le default univ (iInf_le _ univ_mem)
case refine'_2
α : Type u_2
β : Type u_3
γ : Type ?u.23378
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht✝ : t ∈ iInf f
i✝ : ι
s₁✝ s₂✝ : Set α
hs : s₁✝ ∈ f i✝
ht : (⨅ (i : ι), Filter.lift (f i) g) ≤ g s₂✝
⊢ (⨅ (i : ι), Filter.lift (f i) g) ≤ g s₁✝ ⊓ g s₂✝
case refine'_2
α : Type u_2
β : Type u_3
γ : Type ?u.23378
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht✝ : t ∈ iInf f
i✝ : ι
s₁✝ s₂✝ : Set α
hs : s₁✝ ∈ f i✝
ht : (⨅ (i : ι), Filter.lift (f i) g) ≤ g s₂✝
⊢ (⨅ (i : ι), Filter.lift (f i) g) ≤ g (s₁✝ ∩ s₂✝)
rw [hg]
no goals
case refine'_2
α : Type u_2
β : Type u_3
γ : Type ?u.23378
ι : Sort u_1
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Set α → Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht✝ : t ∈ iInf f
i✝ : ι
s₁✝ s₂✝ : Set α
hs : s₁✝ ∈ f i✝
ht : (⨅ (i : ι), Filter.lift (f i) g) ≤ g s₂✝
⊢ (⨅ (i : ι), Filter.lift (f i) g) ≤ g s₁✝ ⊓ g s₂✝
exact le_inf (iInf₂_le_of_le _ _ <| iInf_le _ hs) ht