preimage_mono

Mathlib.Data.PFun

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

English

If s ⊆ t, then f.preimage(s) ⊆ f.preimage(t); preimage is monotone in the set argument.

Русский

Если s ⊆ t, то f.preimage(s) ⊆ f.preimage(t); предобраз монотонен по аргументу множества.

LaTeX

$$$f.preimage(s) \\subseteq f.preimage(t)$$$

Lean4

theorem preimage_mono {s t : Set β} (h : s ⊆ t) : f.preimage s ⊆ f.preimage t :=
  SetRel.preimage_mono h

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

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

Разделы

Аффилиация

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