fintypeInsertOfNotMem — Mathlib

English

If a ∉ s, then insert a s is finite provided s is finite.

Русский

Если a не принадлежит s, то insert a s конечно, если s конечно.

LaTeX

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

Lean4

/-- A `Fintype` structure on `insert a s` when inserting a new element. -/
def fintypeInsertOfNotMem {a : α} (s : Set α) [Fintype s] (h : a ∉ s) : Fintype (insert a s : Set α) :=
  Fintype.ofFinset ⟨a ::ₘ s.toFinset.1, s.toFinset.nodup.cons (by simp [h])⟩ <| by simp

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