LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Every face of a plane subgraph contains each face of the original graph that it meets

Statement

Let $H$ be a plane subgraph of a plane graph $G$ in the inherited drawing (Plane embeddings of finite simple graphs, their faces, facial boundary walks and lengths (counting a bridge twice), and planar graphs, Subgraphs, induced subgraphs and spanning subgraphs). If a face $f_{H}$ of $H$ meets a face $f_{G}$ of $G$ , then $f_{G} \subseteq f_{H}$ .

Facts & Assumptions

Given: Such $G, H, f_{G}, f_{H}$ with $f_{G} \cap f_{H} \neq \emptyset$ .

[L1]

A connected component is the largest connected subset of the ambient space containing any one of its points (Connected components, quasicomponents, and totally disconnected spaces).

Proof

technique · direct

1.1

Since the drawing of $H$ is contained in the drawing of $G$ , its complement contains the complement of $G$ . The face $f_{G}$ is connected and lies wholly in the complement of $H$ .

givenL1

2.1

Choose a point of $f_{G} \cap f_{H}$ . Both sets contain it, and [L1] says $f_{H}$ is the largest connected subset of the complement of $H$ containing it. Step 1.1 therefore gives $f_{G} \subseteq f_{H}$ .

step 1.1L1∎

Depends on

Used by

Every three-connected graph with no K₅ or K_3,3 minor is planar Lemma

Dependency tree · two levels

11 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

R. Diestel, Graph Theory, 6th ed., Lemma 4.2.1 (standard reference, not scraped)