SimpleGraph.farFromTriangleFree.le_card_sub_card

theorem SimpleGraph.farFromTriangleFree.le_card_sub_card : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Fintype α] [inst_1 : LinearOrderedRing 𝕜] {G : SimpleGraph α} {ε : 𝕜}, G.FarFromTriangleFree ε → ∀ ⦃H : SimpleGraph α⦄ [inst_2 : DecidableRel H.Adj], H ≤ G → H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑G.edgeFinset.card - ↑H.edgeFinset.card

This theorem, an alias of the forward direction of `SimpleGraph.farFromTriangleFree_iff`, states that for any types `α` and `𝕜`, with `α` being a finite type and `𝕜` being a linear ordered ring, and any simple graphs `G` and `H` on `α`, if `G` is far from triangle-free with respect to some ε in `𝕜`, `H` is a subgraph of `G`, and `H` is 3-clique-free (i.e., doesn't contain any triangles), then ε times the square of the number of vertices in `α` is less than or equal to the difference of the number of edges in `G` and the number of edges in `H`.

More concisely: If `G` is a simple graph on a finite type `α` with `H` being a 3-clique-free subgraph, and `ε` is a positive number in a linear ordered ring such that the number of edges in `G` is at most `ε * √(#α) * (#α - 2)` edges more than in `H`, then `G` is far from triangle-free with respect to `ε`.