pos — Mathlib

English

Let G be a finite-vertex graph with a density parameter ε and a pair of vertex-sets s,t. If G exhibits ε-uniformity on (s,t), then ε must be strictly positive.

Русский

Пусть граф G имеет пару множеств вершин s,t и параметр плотности ε. Если G обладает ε-однородностью на паре (s,t), то ε положительно.

LaTeX

$$$G \ IsUniform \varepsilon \, s \, t \Rightarrow 0 < \varepsilon$$$

Lean4

theorem pos (hG : G.IsUniform ε s t) : 0 < ε :=
  not_le.1 fun hε ↦
    (hε.trans <| abs_nonneg _).not_gt <|
      hG (empty_subset _) (empty_subset _) (by simpa using mul_nonpos_of_nonneg_of_nonpos (Nat.cast_nonneg _) hε)
        (by simpa using mul_nonpos_of_nonneg_of_nonpos (Nat.cast_nonneg _) hε)

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