mono_left

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.MapsTo.mono_left

English

If f maps s1 to t and s2 ⊆ s1, then f maps s2 to t.

Русский

Если f отображает s1 в t, а s2 ⊆ s1, тогда f отображает s2 в t.

LaTeX

$$$ MapsTo\\ f\\ s_1\\ t \\to s_2 \\subseteq s_1 \\to MapsTo\\ f\\ s_2\\ t $$$

Lean4

theorem mono_left (hf : MapsTo f s₁ t) (hs : s₂ ⊆ s₁) : MapsTo f s₂ t := fun _ hx => hf (hs hx)

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

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

Разделы

Аффилиация

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