finite_sep — Mathlib

English

If S is finite and p is a predicate on the ambient type, then {a in S | p a} is finite.

Русский

Если S конечно, и задан признак p на элементы, то множество {a ∈ S | p a} конечно.

LaTeX

$$$\forall {\alpha : Type u} (s : Set\alpha) (p : \alpha \to Prop), Finite s \to Finite ({a \in s | p a} : Set\alpha)$$$

Lean4

instance finite_sep (s : Set α) (p : α → Prop) [Finite s] : Finite ({a ∈ s | p a} : Set α) :=
  by
  cases nonempty_fintype s
  classical infer_instance

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