property_index

Mathlib.Order.Filter.Bases.Basic

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

English

The index chosen satisfies p.

Русский

Выбор индекса удовлетворяет условию p.

LaTeX

$$$p((h.index t ht).val)$$$

Lean4

theorem property_index (h : l.HasBasis p s) (ht : t ∈ l) : p (h.index t ht) :=
  (h.index t ht).2

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

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

Разделы

Аффилиация

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