subtype_map_of_mem — Mathlib

English

If every x ∈ s satisfies p x, then (s.subtype p).map Embedding.subtype p = s.

Русский

Если каждый x ∈ s удовлетворяет p x, то (s.subtype p).map Embedding.subtype p = s.

LaTeX

$$$ (s.subtype p).map (Embedding.subtype p) = s $$$

Lean4

/-- If all elements of a `Finset` satisfy the predicate `p`,
`s.subtype p` converts back to `s` with `Embedding.subtype`. -/
theorem subtype_map_of_mem {p : α → Prop} [DecidablePred p] {s : Finset α} (h : ∀ x ∈ s, p x) :
    (s.subtype p).map (Embedding.subtype _) = s :=
  ext <| by simpa [subtype_map] using h

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