toSimpleGraphInclusive_mono — Mathlib

English

The map toSimpleGraphInclusive is monotone: if G ≤ H, then toSimpleGraphInclusive(G) ≤ toSimpleGraphInclusive(H).

Русский

Отображение кSimpleGraphInclusive монотонно: если G ≤ H, то toSimpleGraphInclusive(G) ≤ toSimpleGraphInclusive(H).

LaTeX

$$$\\text{Monotone}(\\text{toSimpleGraphInclusive})$$$

Lean4

@[mono]
theorem toSimpleGraphInclusive_mono : Monotone (toSimpleGraphInclusive : _ → SimpleGraph V) :=
  by
  intro _ _ h₁ _ _ h₂
  apply And.intro h₂.1
  cases h₂.2
  · exact Or.inl <| h₁ ‹_›
  · exact Or.inr <| h₁ ‹_›

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