index — Mathlib

English

For t ∈ l, the index h.index t ht yields an i with p i and s i ⊆ t.

Русский

Для t ∈ l индекс h.index t ht дает i с p i и s i ⊆ t.

LaTeX

$$$h.index\,t\,ht : {i : ι // p i}$ with $p((h.index\,t\,ht).val)$ and $s((h.index\,t\,ht).val) \subseteq t$$$

Lean4

/-- Index of a basis set such that `s i ⊆ t` as an element of `Subtype p`. -/
noncomputable def index (h : l.HasBasis p s) (t : Set α) (ht : t ∈ l) : { i : ι // p i } :=
  ⟨(h.mem_iff.1 ht).choose, (h.mem_iff.1 ht).choose_spec.1⟩

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