mem_lift'

Mathlib.Order.Filter.Lift

URI: https://scilib.ai/kg/mathlib#Filter.mem_lift'

← MathLib Explorer

English

If t is a member of f, then h(t) is a member of f.lift' h.

Русский

Если t принадлежит f, то h(t) принадлежит f.lift' h.

LaTeX

$$$ t \\in f \\Rightarrow h(t) \\in f.lift' h $$$

Lean4

theorem mem_lift' {t : Set α} (ht : t ∈ f) : h t ∈ f.lift' h :=
  le_principal_iff.mp <| show f.lift' h ≤ 𝓟 (h t) from iInf_le_of_le t <| iInf_le_of_le ht <| le_rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru