fintypeDiffLeft — Mathlib

English

If s is finite and t is decided by a predicate, then s \\ t is finite.

Русский

Если s конечно, а t задаётся детерминированным предикатом принадлежности, то s \\ t конечно.

LaTeX

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

Lean4

instance fintypeDiffLeft (s t : Set α) [Fintype s] [DecidablePred (· ∈ t)] : Fintype (s \ t : Set α) :=
  Set.fintypeSep s (· ∈ tᶜ)

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