principal_le_lift'

Mathlib.Order.Filter.Lift

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

English

For t ⊆ β, 𝓟 t ≤ f.lift' h iff ∀ s ∈ f, t ⊆ h s.

Русский

Для множества t ⊆ β, 𝓟 t ≤ f.lift' h тогда и только тогда, когда ∀ s ∈ f, t ⊆ h s.

LaTeX

$$$ \\mathcal{P} t \\le f.lift' h \\iff \\forall s \\in f, t \\subseteq h s $$$

Lean4

theorem principal_le_lift' {t : Set β} : 𝓟 t ≤ f.lift' h ↔ ∀ s ∈ f, t ⊆ h s :=
  le_lift'

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

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

Разделы

Аффилиация

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