term_＼_ — Mathlib

English

The deletion M \ D is the restriction of M to E \ D; i.e., M \\ D = M ⟂ (M.E \ D).

Русский

Удаление M \ D определяется как ограничение M на E \ D.

LaTeX

$$M \ D = M ⟂ (M.E \ D)$$

Lean4

/-- `M ＼ D` refers to the deletion of a set `D` from the matroid `M`. -/
@[scoped term_parser 1000]
public meta def «term_＼_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `Matroid.«term_＼_» 75 75
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " ＼ ") (ParserDescr.cat✝ `term 76))

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