set_index_subset

Mathlib.Order.Filter.Bases.Basic

URI: https://scilib.ai/kg/mathlib#Filter.HasBasis.set_index_subset

English

The basis set is contained in t: s(i) ⊆ t.

Русский

Базисный множества включено в t: s(i) ⊆ t.

LaTeX

$$$s((h.index t ht).val) \subseteq t$$$

Lean4

theorem set_index_subset (h : l.HasBasis p s) (ht : t ∈ l) : s (h.index t ht) ⊆ t :=
  (h.mem_iff.1 ht).choose_spec.2

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

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

Разделы

Аффилиация

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