to_subtype — Mathlib

English

Let α be a type and s ⊆ α. If s is finite, then the subtype consisting of exactly the elements of s, i.e., the set {x ∈ α | x ∈ s}, is finite.

Русский

Пусть α — множество (тип). Пусть s ⊆ α конечно. Тогда подтипом s, то есть {x ∈ α | x ∈ s}, является конечное.

LaTeX

$$$ \\text{Finite}(s) \\Rightarrow \\text{Finite}(\\{ x \\in \\alpha \\mid x \\in s \\}) $$$

Lean4

/-- Projection of `Set.Finite` to its `Finite` instance.
This is intended to be used with dot notation.
See also `Set.Finite.Fintype` and `Set.Finite.nonempty_fintype`. -/
protected theorem to_subtype {s : Set α} (h : s.Finite) : Finite s :=
  h

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