induce_mono — Mathlib

English

Inducing with respect to a subgraph is monotone in both arguments: if G' ≤ G'' and s ⊆ s', then G'.induce s ≤ G''.induce s'.

Русский

Индукция по подграфу монотная по обеим переменным: если G' ≤ G'' и s ⊆ s', то G'.induce s ≤ G''.induce s'.

LaTeX

$$$ (hg:\\le) \\ (hs:\\subseteq) \\Rightarrow G'.induce s ≤ G''.induce s' $$$

Lean4

@[gcongr]
theorem induce_mono (hg : G' ≤ G'') (hs : s ⊆ s') : G'.induce s ≤ G''.induce s' :=
  by
  constructor
  · simp [hs]
  · simp +contextual only [induce_adj, and_imp]
    intro v w hv hw ha
    exact ⟨hs hv, hs hw, hg.2 ha⟩

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