infEdist_eq_top_iff — Mathlib

English

InfEdist x s = ∞ together with other equivalences characterize emptiness of s.

Русский

InfEdist x s = ∞ в сочетании с другими эквивалентностями характеризует пустоту s.

LaTeX

$$$ \operatorname{infEdist}(x,s) = \infty \Leftrightarrow s = \varnothing $$$

Lean4

@[simp]
theorem infEdist_eq_top_iff : infEdist x s = ∞ ↔ s = ∅ := by
  rcases s.eq_empty_or_nonempty with rfl | hs <;> simp [*, Nonempty.ne_empty, infEdist_ne_top]

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