fintypeSubset — Mathlib

English

If a set s is finite, then any subset t ⊆ s is finite.

Русский

Если множество s конечное, то любое подмножество t ⊆ s также конечное.

LaTeX

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

Lean4

/-- A `Fintype` structure on a set defines a `Fintype` structure on its subset. -/
def fintypeSubset (s : Set α) {t : Set α} [Fintype s] [DecidablePred (· ∈ t)] (h : t ⊆ s) : Fintype t :=
  by
  rw [← inter_eq_self_of_subset_right h]
  apply Set.fintypeInterOfLeft

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