image_mono

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Set.image_mono

English

`Set.image` is monotone with respect to inclusion.

Русский

Оператор изображения Set.image монотонен относительно включения.

LaTeX

$$$ \\text{Monotone}(\\mathrm{image}\\, f). $$$

Lean4

@[gcongr]
theorem image_mono (h : s ⊆ t) : f '' s ⊆ f '' t := by grind

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

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

Разделы

Аффилиация

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