subtype_map — Mathlib

English

Converting a Finset of elements with property p back to the main type via Embedding.subtype p yields the same as filtering by p.

Русский

Преобразование Finset элементов с свойством p обратно в исходный тип через Embedding.subtype p эквивалентно фильтрации по p.

LaTeX

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

Lean4

/-- `s.subtype p` converts back to `s.filter p` with
`Embedding.subtype`. -/
@[simp]
theorem subtype_map (p : α → Prop) [DecidablePred p] {s : Finset α} :
    (s.subtype p).map (Embedding.subtype _) = s.filter p :=
  by
  ext x
  simp [@and_comm _ (_ = _), @and_comm (p x) (x ∈ s)]

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