map

Mathlib.Order.Filter.Subsingleton

URI: https://scilib.ai/kg/mathlib#Filter.Subsingleton.map

English

If hl : l.Subsingleton, then the image filter map f l is subsingleton.

Русский

Если hl : l.Subsingleton, то образ фильтра map f l также подсинглетен.

LaTeX

$$$hl.Subsingleton \Rightarrow (map f l).Subsingleton$$$

Lean4

theorem map (hl : l.Subsingleton) (f : α → β) : (map f l).Subsingleton :=
  let ⟨s, hsl, hs⟩ := hl;
  ⟨f '' s, image_mem_map hsl, hs.image f⟩

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

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

Разделы

Аффилиация

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