apply_coe_mem_map

Mathlib.Data.Finset.Image

URI: https://scilib.ai/kg/mathlib#Finset.apply_coe_mem_map

English

Let p be a predicate on α. For any x in the subtype p, x ∈ s.subtype p if and only if x.val ∈ s.

Русский

Пусть p — предикат на α. Для любого x из подтипа p верно: x ∈ s.subtype p тогда и только тогда, когда x.val ∈ s.

LaTeX

$$x ∈ s.subtype p \\iff x.1 ∈ s$$

Lean4

theorem apply_coe_mem_map (f : α ↪ β) (s : Finset α) (x : s) : f x ∈ s.map f :=
  mem_map_of_mem f x.prop

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru