instFintypeElemImageToSetOfDecidableEqOfSingletonSet

English

If every singleton image under a relation is finite, then the image of any finite set is finite.

Русский

Если под каждое единственное множество образа применяется множество конечно, то образ любого конечного множества конечен.

LaTeX

$$$\\\\text{If } R\\text{ image}({a})\\text{ is finite for all } a,\\text{ then } R\\text{ image}(A)\\text{ is finite for any finite } A.$$$

Lean4

/-- Given a relation such that the image of every singleton set is finite, then the image of every
finite set is finite. -/
instance {α : Type u} {β : Type v} [DecidableEq β] (R : SetRel α β) [∀ a : α, Fintype (R.image { a })] (A : Finset α) :
    Fintype (R.image A) :=
  by
  have h : R.image A = (A.biUnion fun a => (R.image { a }).toFinset : Set β) :=
    by
    ext
    simp [SetRel.image]
  rw [h]
  apply FinsetCoe.fintype

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