α : Type u
β : Type v
γ : Type ?u.55875
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
⊢ map m (ofComapInfPrincipal h) = g
α : Type u
β : Type v
γ : Type ?u.55875
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
⊢ map m (ofComapInfPrincipal h) = g
let f := Filter.comap m g ⊓ 𝓟 s
α : Type u
β : Type v
γ : Type ?u.55875
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : NeBot f
⊢ map m (ofComapInfPrincipal h) = g
α : Type u
β : Type v
γ : Type ?u.55875
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
⊢ map m (ofComapInfPrincipal h) = g
haveI : f.NeBot := comap_inf_principal_neBot_of_image_mem h
case h
α : Type u
β : Type v
γ : Type ?u.55875
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : NeBot f
⊢ ↑(map m (ofComapInfPrincipal h)) ≤ ↑g
α : Type u
β : Type v
γ : Type ?u.55875
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : NeBot f
⊢ map m (ofComapInfPrincipal h) = g
apply eq_of_le
no goals
case h
α : Type u
β : Type v
γ : Type ?u.55875
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : NeBot f
⊢ ↑(map m (ofComapInfPrincipal h)) ≤ ↑g
calc
  Filter.map m (of f) ≤ Filter.map m f := map_mono (of_le _)
  _ ≤ (Filter.map m <| Filter.comap m g) ⊓ Filter.map m (𝓟 s) := map_inf_le
  _ = (Filter.map m <| Filter.comap m g) ⊓ (𝓟 <| m '' s) := by rw [map_principal]
  _ ≤ ↑g ⊓ (𝓟 <| m '' s) := inf_le_inf_right _ map_comap_le
  _ = ↑g := inf_of_le_left (le_principal_iff.mpr h)
no goals
α : Type u
β : Type v
γ : Type ?u.55875
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : NeBot f
⊢ Filter.map m (Filter.comap m ↑g) ⊓ Filter.map m (𝓟 s) = Filter.map m (Filter.comap m ↑g) ⊓ 𝓟 (m '' s)
rw [map_principal]