le_iff_subset

Mathlib.Order.Closure

URI: https://scilib.ai/kg/mathlib#LowerAdjoint.le_iff_subset

English

For s ⊆ Set β and S ∈ α, l s ≤ S iff s ⊆ S.

Русский

Для множества s ⊆ Set β и S ∈ α верно l s ≤ S тогда и только тогда, когда s ⊆ S.

LaTeX

$$$l(s) \le S \iff s \subseteq S$$$

Lean4

theorem le_iff_subset (s : Set β) (S : α) : l s ≤ S ↔ s ⊆ S :=
  l.gc s S

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

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

Разделы

Аффилиация

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