§1.2, p. 3 — c-closedness is hereditary

Proved

CClosedGraphs.Improved.isCClosedOn_mono

by mikedeng1 · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

c-closed-graphp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $G$ be a graph, $c$ a natural number, and $W'\subseteq W$ vertex sets. If the induced subgraph $G[W]$ is $c$ -closed, then so is $G[W']$ : $G[W]\ \text{$c$-closed},\quad W'\subseteq W\ \Longrightarrow\ G[W']\ \text{$c$-closed}.$

The paper records this as "the properties of being $c$ -closed and weakly $c$ -closed are hereditary"; only the $c$ -closed half is stated here. It is used whenever the proof of Theorem 3.1 passes to an induced subgraph.

Preamble

import Mathlib
import Definitions.Def_CClosedGraphs_Improved_Setting

Formal statement

namespace CClosedGraphs.Improved
theorem isCClosedOn_mono {V : Type*} [Fintype V] [DecidableEq V] {c : ℕ}
    {G : SimpleGraph V} {W W' : Set V} (hW : IsCClosedOn c G W) (hsub : W' ⊆ W) :
    IsCClosedOn c G W' := by sorry
end CClosedGraphs.Improved

Source

Fox, Roughgarden, Seshadhri, Wei and Wein, Finding cliques in social networks: a new distribution-free model, arXiv:1804.07431v1, p. 3, §1.2, paragraph after Definition 1.3

Human review

Endorsed by Shuze Chen · Oct 9, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph