mono

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.LeftInvOn.mono

English

If hf is left inverse on s and s₁ ⊆ s, then hf is left inverse on s₁.

Русский

Если hf — левый обратный на s и s₁ ⊆ s, то hf — левый обратный на s₁.

LaTeX

$$$$ \\text{LeftInvOn } f' f s \\;\\wedge\\; s_1 \\subseteq s \\Rightarrow \\text{LeftInvOn } f' f s_1. $$$$

Lean4

theorem mono (hf : LeftInvOn f' f s) (ht : s₁ ⊆ s) : LeftInvOn f' f s₁ := fun _ hx => hf (ht hx)

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

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

Разделы

Аффилиация

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