monotone_image

Mathlib.Data.Set.Image

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

← MathLib Explorer

English

The image operator is monotone: if s ⊆ t then f '' s ⊆ f '' t.

Русский

Оператор изображения монотонен: если s ⊆ t, то f '' s ⊆ f '' t.

LaTeX

$$$ s \\subseteq t \\Rightarrow f''s \\subseteq f''t. $$$

Lean4

/-- `Set.image` is monotone. See `Set.image_mono` for the statement in terms of `⊆`. -/
theorem monotone_image : Monotone (image f) := fun _ _ => image_mono

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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