IsCoinitialFor — Mathlib

English

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

Русский

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

LaTeX

$$$ IsCoinitialFor(s,t) := \\forall \\{a\\}, a \\in s → ∃ b ∈ t, b ≤ a$$$

Lean4

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

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