ofComapInfPrincipal_eq_of_map — Mathlib

English

(map m) ofComapInfPrincipal h equals g.

Русский

(map m)(ofComapInfPrincipal h) равно g.

LaTeX

$$$(\\mathrm{map}\\ m)(\\mathrm{ofComapInfPrincipal}\\ h) = g$$$

Lean4

theorem ofComapInfPrincipal_eq_of_map (h : m '' s ∈ g) : (ofComapInfPrincipal h).map m = g :=
  by
  let f := Filter.comap m g ⊓ 𝓟 s
  haveI : f.NeBot := comap_inf_principal_neBot_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)

Похожие утверждения