of_le

Mathlib.Combinatorics.SimpleGraph.Copy

URI: https://scilib.ai/kg/mathlib#SimpleGraph.IsContained.of_le

English

If G1 ≤ G2 then G1 ⊑ G2.

Русский

Если G1 содержится в G2, то G1 содержится в G2.

LaTeX

$$G1 ≤ G2 → G1 ⊑ G2$$

Lean4

/-- A simple graph contains its subgraphs. -/
theorem of_le (h : G₁ ≤ G₂) : G₁ ⊑ G₂ :=
  ⟨.ofLE G₁ G₂ h⟩

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

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

Разделы

Аффилиация

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