fromEdgeSet_mono — Mathlib

English

If s ⊆ t then fromEdgeSet s ≤ fromEdgeSet t (in the graph order).

Русский

Если s ⊆ t, то fromEdgeSet s ≤ fromEdgeSet t.

LaTeX

$$$\\,s \\subseteq t \\Rightarrow \\mathrm{fromEdgeSet}(s) \\le \\mathrm{fromEdgeSet}(t)$$$

Lean4

@[gcongr, mono]
theorem fromEdgeSet_mono {s t : Set (Sym2 V)} (h : s ⊆ t) : fromEdgeSet s ≤ fromEdgeSet t :=
  by
  rintro v w
  simp +contextual only [fromEdgeSet_adj, Ne, not_false_iff, and_true, and_imp]
  exact fun vws _ => h vws

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