map_subtype_subset — Mathlib

English

Let t be a subset of α. For any Finset s of elements of t, the image of s under the inclusion map t → α is contained in t.

Русский

Пусть t ⊆ α. Для любого финсетa s, состоящего из элементов t, образ s через включение t в α содержится в t.

LaTeX

$$$\\iota_t(s) \\subseteq t$, where $\\iota_t: t \\hookrightarrow \\alpha$ is the inclusion.$$

Lean4

/-- If a `Finset` of a subtype is converted to the main type with
`Embedding.subtype`, the result is a subset of the set giving the
subtype. -/
theorem map_subtype_subset {t : Set α} (s : Finset t) : ↑(s.map (Embedding.subtype _)) ⊆ t :=
  by
  intro a ha
  rw [mem_coe] at ha
  convert property_of_mem_map_subtype s ha

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