mono_right

Mathlib.Data.Set.Function

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

English

If f maps s to t1 and t1 ⊆ t2, then f maps s to t2.

Русский

Если f отображает s в t1, а t1 ⊆ t2, то f отображает s в t2.

LaTeX

$$$ MapsTo\\ f\\ s\\ t_1 \\to t_1 \\subseteq t_2 \\to MapsTo\\ f\\ s\\ t_2 $$$

Lean4

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

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

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

Разделы

Аффилиация

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