top_isIndContained_iff_top_isContained

English

The induced containment relation for the complete graph on V aligns with ordinary containment for the top graph.

Русский

Индуктивное вложение полного графа на V совпадает с обычным вложением для верхнего графа.

LaTeX

$$$(\top : SimpleGraph V) \subseteq_{\mathrm{ind}} H \iff (\top : SimpleGraph V) \subseteq H$$$

Lean4

@[simp]
theorem top_isIndContained_iff_top_isContained : (⊤ : SimpleGraph V) ⊴ H ↔ (⊤ : SimpleGraph V) ⊑ H :=
  ⟨IsIndContained.isContained, fun ⟨f⟩ ↦ ⟨f.topEmbedding⟩⟩

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