lt_extremalNumber_iff_of_nonneg — Mathlib

English

If 0 ≤ m, then m < extremalNumber(card V) H iff there exists G with H.Free G and m < |G.edgeFinset|.

Русский

Если 0 ≤ m, то $m < \\mathrm{extremalNumber}(card V,H)$ эквивалентно существованию $G$ с $H.Free G$ и $m < |G.edgeFinset|$.

LaTeX

$$\$ m \\ge 0 \\Rightarrow m < \\mathrm{extremalNumber}(\\mathrm{card} V, H) \\iff \\exists G, H.Free G \\land m < |G.edgeFinset| \$$$

Lean4

@[inherit_doc lt_extremalNumber_iff]
theorem lt_extremalNumber_iff_of_nonneg (H : SimpleGraph W) {m : R} (h : 0 ≤ m) :
    m < extremalNumber (card V) H ↔ ∃ G : SimpleGraph V, ∃ _ : DecidableRel G.Adj, H.Free G ∧ m < #G.edgeFinset :=
  by
  simp_rw [← Nat.floor_lt h]
  exact lt_extremalNumber_iff H ⌊m⌋₊

Похожие утверждения