IsCofinal — Mathlib

English

Let α be a poset with a ≤ relation. A subset s ⊆ α is cofinal if for every x in α there exists y in s with x ≤ y.

Русский

Пусть α является частично упорядоченным множеством с отношением ≤. Подмножество s ⊆ α кофинально, если для любого x ∈ α существует y ∈ s такой, что x ≤ y.

LaTeX

$$$IsCofinal(s) \iff \forall x \; \exists y \,(y \in s \land x \le y)$$$

Lean4

/-- A set is cofinal when for every `x : α` there exists `y ∈ s` with `x ≤ y`. -/
def IsCofinal (s : Set α) : Prop :=
  ∀ x, ∃ y ∈ s, x ≤ y

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