fintypeDiff — Mathlib

English

If s and t are finite subsets of α, then the set difference s \\ t is finite.

Русский

Если s и t конечны, то s \\ t также конечно.

LaTeX

$$$\\forall \\alpha\\, (s,t : \\text{Set }\\alpha),\\; \\operatorname{Finite}(s) \\land \\operatorname{Finite}(t) \\Rightarrow \\operatorname{Finite}(s \\setminus t).$$$

Lean4

instance fintypeDiff [DecidableEq α] (s t : Set α) [Fintype s] [Fintype t] : Fintype (s \ t : Set α) :=
  Fintype.ofFinset (s.toFinset \ t.toFinset) <| by simp

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