ofComapInfPrincipal_mem — Mathlib

English

If h holds, then s ∈ OfComapInfPrincipal h.

Русский

Если выполнено h, то s принадлежит OfComapInfPrincipal h.

LaTeX

$$$ (h) \\Rightarrow s \\in \\mathrm{ofComapInfPrincipal}(h)$$$

Lean4

theorem ofComapInfPrincipal_mem (h : m '' s ∈ g) : s ∈ ofComapInfPrincipal h :=
  by
  let f := Filter.comap m g ⊓ 𝓟 s
  haveI : f.NeBot := comap_inf_principal_neBot_of_image_mem h
  have : s ∈ f := mem_inf_of_right (mem_principal_self s)
  exact le_def.mp (of_le _) s this

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