filterMap_mono

Mathlib.Data.Finset.Image

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

English

If s ⊆ t then filterMap f s f_inj ⊆ filterMap f t f_inj.

Русский

Если s ⊆ t, то filterMap f s f_inj ⊆ filterMap f t f_inj.

LaTeX

$$$ s \\subseteq t \\Rightarrow (s.filterMap f f_{inj}) \\subseteq (t.filterMap f f_{inj}) $$$

Lean4

theorem filterMap_mono (h : s ⊆ t) : filterMap f s f_inj ⊆ filterMap f t f_inj := by grind

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

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

Разделы

Аффилиация

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