gauge_pos — Mathlib

English

0 < gauge s x iff x ≠ 0, given absorbent and von N-bounded s and topological assumptions.

Русский

0 < gauge s x тогда и только тогда x ≠ 0, при условии абсорбированности, ограниченности и топологических условий.

LaTeX

$$$$0 < \\mathrm{gauge}(s,x) \\iff x \\neq 0.$$$$

Lean4

theorem gauge_pos (hs : Absorbent ℝ s) (hb : Bornology.IsVonNBounded ℝ s) : 0 < gauge s x ↔ x ≠ 0 := by
  simp only [(gauge_nonneg _).lt_iff_ne', Ne, gauge_eq_zero hs hb]

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