image_congr'

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Set.image_congr'

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

/-- A common special case of `image_congr` -/
theorem image_congr' {f g : α → β} {s : Set α} (h : ∀ x : α, f x = g x) : f '' s = g '' s := by grind

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

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

Разделы

Аффилиация

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