monotone_preimage

Mathlib.Data.Set.Lattice.Image

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

English

For any function f, the preimage operator is monotone: if A ⊆ B then f^{-1}(A) ⊆ f^{-1}(B).

Русский

Для всякой функции f предобразование множеств монотно по включению: если A ⊆ B, то f^{-1}(A) ⊆ f^{-1}(B).

LaTeX

$$$A \subseteq B \implies f^{-1}(A) \subseteq f^{-1}(B)$$$

Lean4

theorem monotone_preimage {f : α → β} : Monotone (preimage f) := fun _ _ h => preimage_mono h

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

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

Разделы

Аффилиация

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