image_mono

Mathlib.Data.Finset.Image

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

English

The map s ↦ s.image f is monotone: if s ⊆ t then s.image f ⊆ t.image f.

Русский

Отображение s ↦ s.image f монотонно: если s ⊆ t, то s.image f ⊆ t.image f.

LaTeX

$$$\forall s,t,\; s \subseteq t \Rightarrow s.image f \subseteq t.image f$$$

Lean4

theorem image_mono (f : α → β) : Monotone (Finset.image f) := fun _ _ => image_subset_image

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

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

Разделы

Аффилиация

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