finite_insert — Mathlib

English

A set is finite after inserting a into it if and only if the original set was finite.

Русский

Множество является конечным после вставки элемента a тогда и только тогда, когда исходное множество было конечным.

LaTeX

$$$\mathrm{Finite}(\{a\} \cup s) \iff \mathrm{Finite}(s)$$$

Lean4

@[simp]
theorem finite_insert : (insert a s).Finite ↔ s.Finite
    where
  mp hs := hs.subset <| subset_insert ..
  mpr := .insert _

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