isUniform_singleton — Mathlib

English

For singleton blocks {a} and {b}, ε-uniformity of G on ({a},{b}) is equivalent to ε > 0.

Русский

Для блоков-одиночек {a} и {b} ε-однородность графа G на ({a},{b}) эквивалентна тому, что ε > 0.

LaTeX

$$$G \ IsUniform \varepsilon \{a\} \{b\} \iff 0 < \varepsilon$$$

Lean4

@[simp]
theorem isUniform_singleton : G.IsUniform ε { a } { b } ↔ 0 < ε :=
  by
  refine ⟨IsUniform.pos, fun hε s' hs' t' ht' hs ht ↦ ?_⟩
  rw [card_singleton, Nat.cast_one, one_mul] at hs ht
  obtain rfl | rfl := Finset.subset_singleton_iff.1 hs'
  · replace hs : ε ≤ 0 := by simpa using hs
    exact (hε.not_ge hs).elim
  obtain rfl | rfl := Finset.subset_singleton_iff.1 ht'
  · replace ht : ε ≤ 0 := by simpa using ht
    exact (hε.not_ge ht).elim
  · rwa [sub_self, abs_zero]

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