principal_mono

Mathlib.Order.Filter.Basic

URI: https://scilib.ai/kg/mathlib#Filter.principal_mono

English

For sets s and t, 𝓟 s ≤ 𝓟 t iff s ⊆ t.

Русский

Для множеств s и t верно, что 𝓟 s ≤ 𝓟 t тогда и только тогда, когда s ⊆ t.

LaTeX

$$$𝓟 s \le 𝓟 t \iff s \subseteq t$$$

Lean4

theorem principal_mono {s t : Set α} : 𝓟 s ≤ 𝓟 t ↔ s ⊆ t := by simp only [le_principal_iff, mem_principal]

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

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

Разделы

Аффилиация

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