fintypeInsertOfMem — Mathlib

English

If a ∈ s, then insert a s has finite structure (same as s).

Русский

Если a ∈ s, то insert a s имеет ту же конечность, что и s.

LaTeX

$$$\\forall a\\,\\forall s\\,(h:\\, a\\in s),\\operatorname{Finite}(s) \\Rightarrow \\operatorname{Finite}(\\operatorname{insert}(a,s)).$$$

Lean4

/-- A `Fintype` structure on `insert a s` when inserting a pre-existing element. -/
def fintypeInsertOfMem {a : α} (s : Set α) [Fintype s] (h : a ∈ s) : Fintype (insert a s : Set α) :=
  Fintype.ofFinset s.toFinset <| by simp [h]

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