α : Type u
β : Type v
γ : Type ?u.55399
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
⊢ s ∈ ofComapInfPrincipal h
α : Type u
β : Type v
γ : Type ?u.55399
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
⊢ s ∈ ofComapInfPrincipal h
let f := Filter.comap m g ⊓ 𝓟 s
α : Type u
β : Type v
γ : Type ?u.55399
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : NeBot f
⊢ s ∈ ofComapInfPrincipal h
α : Type u
β : Type v
γ : Type ?u.55399
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
⊢ s ∈ ofComapInfPrincipal h
haveI : f.NeBot := comap_inf_principal_neBot_of_image_mem h
α : Type u
β : Type v
γ : Type ?u.55399
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this✝ : NeBot f
this : s ∈ f
⊢ s ∈ ofComapInfPrincipal h
α : Type u
β : Type v
γ : Type ?u.55399
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : NeBot f
⊢ s ∈ ofComapInfPrincipal h
have : s ∈ f := mem_inf_of_right (mem_principal_self s)
no goals
α : Type u
β : Type v
γ : Type ?u.55399
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this✝ : NeBot f
this : s ∈ f
⊢ s ∈ ofComapInfPrincipal h
exact le_def.mp (of_le _) s this