le_egauge_iff — Mathlib

English

For any r, r ≤ egauge(s,x) if and only if for all c, x ∈ c · s implies r ≤ ∥c∥_e.

Русский

Для любого r выполняется r ≤ egauge(s,x) тогда и только если для всех c, x ∈ c · s влечёт r ≤ ∥c∥_e.

LaTeX

$$$r \le \mathrm{egauge}_{\mathbb{K}}(s,x) \iff \forall c,\ x \in c\cdot s \rightarrow r \le \|c\|_e$$$

Lean4

theorem le_egauge_iff : r ≤ egauge 𝕜 s x ↔ ∀ c : 𝕜, x ∈ c • s → r ≤ ‖c‖ₑ :=
  le_iInf₂_iff

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