pimage_mono

Mathlib.Data.Finset.PImage

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

English

If s ⊆ t then s.pimage f ⊆ t.pimage f.

Русский

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

LaTeX

$$s ⊆ t → s.pimage f ⊆ t.pimage f.$$

Lean4

@[mono]
theorem pimage_mono (h : s ⊆ t) : s.pimage f ⊆ t.pimage f :=
  pimage_subset.2 fun x hx _ hy => mem_pimage.2 ⟨x, h hx, hy⟩

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

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

Разделы

Аффилиация

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