toSimpleGraphStrict_mono — Mathlib

English

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

Русский

Функция toSimpleGraphStrict монотонна: если G ≤ H, то toSimpleGraphStrict(G) ≤ toSimpleGraphStrict(H).

LaTeX

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

Lean4

@[mono]
theorem toSimpleGraphStrict_mono : Monotone (toSimpleGraphStrict : _ → SimpleGraph V) := fun _ _ h₁ _ _ h₂ ↦
  And.intro h₂.1 <| And.intro (h₁ h₂.2.1) (h₁ h₂.2.2)

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