card_uIcc — Mathlib

English

There is a finite-type instance for Set.Ioc a b, with elements corresponding to Finset.Ioc a b.

Русский

Для Set.Ioc a b существует инстанс конечного типа с элементами, соответствующими Finset.Ioc a b.

LaTeX

$$Fintype (Set.Ioc a b)$$

Lean4

@[simp]
theorem _root_.Fintype.card_uIcc (a b : α) [Fintype (Set.uIcc a b)] : Fintype.card (Set.uIcc a b) = #(uIcc a b) :=
  Fintype.card_of_finset' _ fun _ ↦ by simp [Set.uIcc]

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