term[[_,_]] — Mathlib

English

The set-theoretic image of uIcc via Finset equals Set.uIcc.

Русский

Образ множества uIcc через Finset равен Set.uIcc.

LaTeX

$$(Finset.uIcc a b : Set α) = Set.uIcc a b$$

Lean4

@[inherit_doc Finset.uIcc, scoped term_parser 1000]
public meta def «term[[_,_]]» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `FinsetInterval.«term[[_,_]]» 1024
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "[[") (ParserDescr.cat✝ `term 0))
          (ParserDescr.symbol✝ ", "))
        (ParserDescr.cat✝ `term 0))
      (ParserDescr.symbol✝ "]]"))

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