_aux_Mathlib_Order_Interval_Finset_Defs___macroRules_FinsetInterval_term[[_,_]]_1

English

If Set.uIcc a b is finite, its cardinality equals the finset's card of uIcc a b.

Русский

Если множество Set.uIcc a b конечно, его кардинал равен кардиналу Finset.uIcc a b.

LaTeX

$$Fintype.card (Set.uIcc a b) = #(uIcc a b)$$

Lean4

@[scoped macro FinsetInterval.«term[[_,_]]»]
public meta def «_aux_Mathlib_Order_Interval_Finset_Defs___macroRules_FinsetInterval_term[[_,_]]_1» : Macro✝ := fun
  | `([[$a, $b]]) => ``(Finset.uIcc $a $b)
  | _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝

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