English
DeleteFar p r is equivalent to a universal bound: for every H ≤ G, if p(H) then r ≤ |G.edgeFinset| − |H.edgeFinset|.
Русский
DeleteFar p r эквивалентно универсальному ограничению: для каждого H ≤ G, если p(H), то r ≤ |G.edgeFinset| − |H.edgeFinset|.
LaTeX
$$$ G.DeleteFar p r \iff \forall H [DecidableRel H.Adj], H \le G \to p(H) \to r \le |G.edgeFinset| - |H.edgeFinset| $$$
Lean4
theorem deleteFar_iff [Fintype (Sym2 V)] :
G.DeleteFar p r ↔ ∀ ⦃H : SimpleGraph _⦄ [DecidableRel H.Adj], H ≤ G → p H → r ≤ #G.edgeFinset - #H.edgeFinset := by
classical
refine ⟨fun h H _ hHG hH ↦ ?_, fun h s hs hG ↦ ?_⟩
· have := h (sdiff_subset (t := H.edgeFinset))
simp only [deleteEdges_sdiff_eq_of_le hHG, edgeFinset_mono hHG, card_sdiff_of_subset, card_le_card, coe_sdiff,
coe_edgeFinset, Nat.cast_sub] at this
exact this hH
·
classical
simpa [card_sdiff_of_subset hs, edgeFinset_deleteEdges, -Set.toFinset_card, Nat.cast_sub, card_le_card hs] using
h (G.deleteEdges_le s) hG
