not_bounded_iff — Mathlib

English

¬Bounded r s is equivalent to Unbounded r s.

Русский

Неограниченность эквивалентна неограниченности по определению; то есть ¬Bounded r s эквивалентно Unbounded r s.

LaTeX

$$¬Bounded(r,s) ↔ Unbounded(r,s)$$

Lean4

@[simp]
theorem not_bounded_iff {r : α → α → Prop} (s : Set α) : ¬Bounded r s ↔ Unbounded r s := by
  simp only [Bounded, Unbounded, not_forall, not_exists, exists_prop]

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