mono

Mathlib.Combinatorics.SimpleGraph.DeleteEdges

URI: https://scilib.ai/kg/mathlib#SimpleGraph.DeleteFar.mono

English

If G.DeleteFar p r2 holds and r1 ≤ r2, then G.DeleteFar p r1 holds as well.

Русский

Если выполняется DeleteFar для r2, и r1 меньше или равно r2, то выполняется также DeleteFar для r1.

LaTeX

$$$ G.DeleteFar p r_2 \Rightarrow (r_1 \le r_2) \Rightarrow G.DeleteFar p r_1 $$$

Lean4

theorem mono (h : G.DeleteFar p r₂) (hr : r₁ ≤ r₂) : G.DeleteFar p r₁ := fun _ hs hG => hr.trans <| h hs hG

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

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

Разделы

Аффилиация

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