Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 HH be a plane subgraph of a plane graph GG 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 fHf_H of HH meets a face fGf_G of GG, then fG⊆fHf_G\subseteq f_H.

Facts & Assumptions

Given: Such G,H,fG,fHG,H,f_G,f_H with fG∩fH≠∅f_G\cap f_H\ne\varnothing.

[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 HH is contained in the drawing of GG, its complement contains the complement of GG. The face fGf_G is connected and lies wholly in the complement of HH.

givenL1
2.1

Choose a point of fG∩fHf_G\cap f_H. Both sets contain it, and [L1] says fHf_H is the largest connected subset of the complement of HH containing it. Step 1.1 therefore gives fG⊆fHf_G\subseteq f_H.

step 1.1L1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 31 results over 13 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources