mem_lift — Mathlib

English

Let f be a filter on α and g a map t ↦ Filter β. If t ∈ f and s ∈ g(t), then s ∈ f.lift g.

Русский

Пусть f — фильтр на α и g: Set α → Filter β. Если t ∈ f и s ∈ g(t), то s ∈ f.lift g.

LaTeX

$$$t \in f \land s \in g(t) \Rightarrow s \in f.lift g$$$

Lean4

theorem mem_lift {s : Set β} {t : Set α} (ht : t ∈ f) (hs : s ∈ g t) : s ∈ f.lift g :=
  le_principal_iff.mp <| show f.lift g ≤ 𝓟 s from iInf_le_of_le t <| iInf_le_of_le ht <| le_principal_iff.mpr hs

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