isMaximalIndepSet_iff — Mathlib

English

Maximal G.IsIndepSet s is equivalent to G.IsIndepSet s together with a maximality condition for all t.

Русский

Максимальная независимая подстановка аналогична независимому множеству вместе с условием максимальности для всех t.

LaTeX

$$Maximal G.IsIndepSet s ↔ G.IsIndepSet s ∧ ∀ t, G.IsIndepSet t → s ⊆ t → t ⊆ s$$

Lean4

/-- An independent set in a graph `G` that cannot be extended by adding more vertices. -/
theorem isMaximalIndepSet_iff {s : Set α} :
    Maximal G.IsIndepSet s ↔ G.IsIndepSet s ∧ ∀ t : Set α, G.IsIndepSet t → s ⊆ t → t ⊆ s :=
  Iff.rfl

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