not_isCofinal_iff — Mathlib

English

In a linear order, s is not cofinal iff s is bounded above; i.e., not isCofinal s iff there exists x with y ≤ x for all y ∈ s.

Русский

В линейном порядке s не софинально тогда и только тогда, когда верхняя граница существет.

LaTeX

$$¬IsCofinal s ↔ ∃ x, ∀ y ∈ s, y < x$$

Lean4

theorem not_isCofinal_iff {s : Set α} : ¬IsCofinal s ↔ ∃ x, ∀ y ∈ s, y < x := by simp [IsCofinal]

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