gauge_le_of_mem — Mathlib

English

If a ≥ 0 and x ∈ a s, then gauge(s,x) ≤ a.

Русский

Если a ≥ 0 и x ∈ a s, то gauge(s,x) ≤ a.

LaTeX

$$$$ a \\ge 0 \\quad\\text{and}\\quad x \\in a\\,s \\Rightarrow \\operatorname{gauge}(s,x) \\le a. $$$$

Lean4

theorem gauge_le_of_mem (ha : 0 ≤ a) (hx : x ∈ a • s) : gauge s x ≤ a :=
  by
  obtain rfl | ha' := ha.eq_or_lt
  · rw [mem_singleton_iff.1 (zero_smul_set_subset _ hx), gauge_zero]
  · exact csInf_le gauge_set_bddBelow ⟨ha', hx⟩

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