[_]_ — Mathlib

English

If t is finite and s ⊆ span t with LIOn on s, then there exists a finite h ⊆ s with card(h) ≤ card(t).

Русский

Если t конечно, и s ⊆ span t при LIOn на s, то существует конечное h ⊆ s такое, что |h| ≤ |t|.

LaTeX

$$$$\exists h: s.Finite, h.toFinset.card \leq t.toFinset.card.$$$$

Lean4

@[inherit_doc LinearPMap, term_parser 1000]
public meta def «term_→ₗ.[_]_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `«term_→ₗ.[_]_» 25 0
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " →ₗ.[") (ParserDescr.cat✝ `term 25))
        (ParserDescr.symbol✝ "] "))
      (ParserDescr.cat✝ `term 0))

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