set_index_mem

Mathlib.Order.Filter.Bases.Basic

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

English

The basis set corresponding to the index is in l.

Русский

Множество, соответствующее индексу, принадлежит фильтру l.

LaTeX

$$$s((h.index t ht).val) \in l$$$

Lean4

theorem set_index_mem (h : l.HasBasis p s) (ht : t ∈ l) : s (h.index t ht) ∈ l :=
  h.mem_of_mem <| h.property_index _

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

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

Разделы

Аффилиация

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