preimage_mono

Mathlib.Data.Set.Image

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

English

If s ⊆ t then f^{-1}(s) ⊆ f^{-1}(t).

Русский

Если s ⊆ t, то f^{-1}(s) ⊆ f^{-1}(t).

LaTeX

$$$s \subseteq t \Rightarrow f^{-1}(s) \subseteq f^{-1}(t).$$$

Lean4

@[gcongr]
theorem preimage_mono {s t : Set β} (h : s ⊆ t) : f ⁻¹' s ⊆ f ⁻¹' t := fun _ hx => h hx

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

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

Разделы

Аффилиация

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