def SimpleGraph.acyclic {V : Type} (G : SimpleGraph V) : Prop

Equations

• G.acyclic = ∀ (v : V) (p : G.Walk v v), ¬p.IsCircuit

def SimpleGraph.connected {V : Type} (G : SimpleGraph V) : Prop

Equations

• G.connected = Nonempty ((v w : V) → G.Walk v w)

def subsetsOfLength {α : Type} : ℕ → List α → List (List α)

Equations

• subsetsOfLength 0 x✝ = [[]]
• subsetsOfLength n.succ [] = []
• subsetsOfLength n.succ (x_2 :: xs) = List.map (List.cons x_2) (subsetsOfLength n xs) ++ subsetsOfLength (n + 1) xs

theorem subsetsOfLengthSubset {α : Type} (n : ℕ) (xs l : List α) : l ∈ subsetsOfLength n xs → l ⊆ xs

def graph₁ : SimpleGraph (Fin 4)

Equations

• graph₁ = SimpleGraph.fromRel fun (x y : Fin 4) => (!↑x == ↑y) = true