mono

Mathlib.Logic.Function.DependsOn

URI: https://scilib.ai/kg/mathlib#DependsOn.mono

English

If f depends on a set s and s ⊆ t, then f depends on t as well.

Русский

Если функция зависит от множества s и s ⊆ t, то она зависит и от t.

LaTeX

$$$s \subseteq t \Rightarrow DependsOn f s \Rightarrow DependsOn f t$$$

Lean4

theorem mono {s t : Set ι} (hst : s ⊆ t) (hf : DependsOn f s) : DependsOn f t := fun _ _ h ↦ hf fun i hi ↦ h i (hst hi)

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

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

Разделы

Аффилиация

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