IsCofinalFor — Mathlib

English

IsCofinalFor(s,t) means: for every a ∈ s there exists b ∈ t with a ≤ b; i.e., s is cofinal in t.

Русский

IsCofinalFor(s,t) означает: для каждого a ∈ s существует b ∈ t с a ≤ b; то есть s является кофиналом относительно t.

LaTeX

$$$ IsCofinalFor(s,t) := \\forall \\{a\\}, a \\in s \\rightarrow \\exists b \\in t, a \\le b$$$

Lean4

/-- A set `s` is said to be cofinal for a set `t` if, for all `a ∈ s` there exists `b ∈ t`
such that `a ≤ b`. -/
def IsCofinalFor (s t : Set α) :=
  ∀ ⦃a⦄, a ∈ s → ∃ b ∈ t, a ≤ b

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