exists_subset_part_bijOn — Mathlib

English

There exists r ⊆ s such that P.part restricted to r is bijective onto P.parts.

Русский

Существует r ⊆ s такое, что P.part, ограниченное до r, является биекцией на P.parts.

LaTeX

$$$ \exists r \subseteq s,\ BijOn(P.part, r, P.parts) $$$

Lean4

theorem exists_subset_part_bijOn : ∃ r ⊆ s, Set.BijOn P.part r P.parts :=
  by
  obtain ⟨r, hrs, hr⟩ := P.part_surjOn.exists_bijOn_subset
  lift r to Finset α using s.finite_toSet.subset hrs
  exact ⟨r, mod_cast hrs, hr⟩

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