feat(order/filter/ultrafilter): add some comap_inf_principal lemmas (#…

…11495)

...in the setting of ultrafilters

These lemmas are useful to prove e.g. that the continuous image of a
compact set is compact in the setting of convergence spaces.


Co-authored-by: Patrick Massot <patrickmassot@free.fr>

src/order/filter/ultrafilter.lean

@@ -50,8 +50,11 @@ instance ne_bot (f : ultrafilter α) : ne_bot (f : filter α) := f.ne_bot'
 lemma coe_injective : injective (coe : ultrafilter α → filter α)
 | ⟨f, h₁, h₂⟩ ⟨g, h₃, h₄⟩ rfl := by congr
 
+lemma eq_of_le {f g : ultrafilter α} (h : (f : filter α) ≤ g) : f = g :=
+coe_injective (g.unique h)
+
 @[simp, norm_cast] lemma coe_le_coe {f g : ultrafilter α} : (f : filter α) ≤ g ↔ f = g :=
-⟨λ h, coe_injective $ g.unique h, λ h, h ▸ le_rfl⟩
+⟨λ h, eq_of_le h, λ h, h ▸ le_rfl⟩
 
 @[simp, norm_cast] lemma coe_inj : (f : filter α) = g ↔ f = g := coe_injective.eq_iff
 
@@ -313,3 +316,40 @@ compl_compl s ▸ hf.compl_mem_hyperfilter
 end hyperfilter
 
 end filter
+
+namespace ultrafilter
+
+open filter
+
+variables {m : α → β} {s : set α} {g : ultrafilter β}
+
+lemma comap_inf_principal_ne_bot_of_image_mem (h : m '' s ∈ g) :
+  (filter.comap m g ⊓ 𝓟 s).ne_bot :=
+filter.comap_inf_principal_ne_bot_of_image_mem g.ne_bot h
+
+/-- Ultrafilter extending the inf of a comapped ultrafilter and a principal ultrafilter. -/
+noncomputable def of_comap_inf_principal (h : m '' s ∈ g) : ultrafilter α :=
+@of _ (filter.comap m g ⊓ 𝓟 s) (comap_inf_principal_ne_bot_of_image_mem h)
+
+lemma of_comap_inf_principal_mem (h : m '' s ∈ g) : s ∈ of_comap_inf_principal h :=
+begin
+  let f := filter.comap m g ⊓ 𝓟 s,
+  haveI : f.ne_bot := comap_inf_principal_ne_bot_of_image_mem h,
+  have : s ∈ f := mem_inf_of_right (mem_principal_self s),
+  exact le_def.mp (of_le _) s this
+end
+
+lemma of_comap_inf_principal_eq_of_map (h : m '' s ∈ g) :
+  (of_comap_inf_principal h).map m = g :=
+begin
+  let f := filter.comap m g ⊓ 𝓟 s,
+  haveI : f.ne_bot := comap_inf_principal_ne_bot_of_image_mem h,
+  apply eq_of_le,
+  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)
+end
+
+end ultrafilter