subtypeEquivToFinset — Mathlib

English

There is a canonical equivalence between the subtype {x | x ∈ s} and the subtype {x | x ∈ hs.toFinset}.

Русский

Существует каноническое эквивалентное отображение между подтипами {x | x ∈ s} и {x | x ∈ hs.toFinset}.

LaTeX

$$$$ \\{ x \\mid x \\in s \\} \\simeq \\{ x \\mid x \\in hs.toFinset \\}. $$$$

Lean4

/-- The identity map, bundled as an equivalence between the subtypes of `s : Set α` and of
`h.toFinset : Finset α`, where `h` is a proof of finiteness of `s`. -/
@[simps!]
def subtypeEquivToFinset : { x // x ∈ s } ≃ { x // x ∈ hs.toFinset } :=
  (Equiv.refl α).subtypeEquiv fun _ ↦ hs.mem_toFinset.symm

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