rightDual — Mathlib

English

RightDual maps any set I ⊆ β to { a ∈ α | ∀ b ∈ I, a ~[R] b }.

Русский

RightDual отображает любой набор I ⊆ β в { a ∈ α | ∀ b ∈ I, a ~R b }.

LaTeX

$$$\mathrm{rightDual}(I) = \{ a \in \alpha \mid \forall b \in I,\ a \;\tilde{R}\; b \}.$$$

Lean4

/-- `rightDual` maps any set `I` of elements of type `β` to the set `{a : α | ∀ b ∈ I, a ~[R] b}`
of elements `a` of type `α` such that `a ~[R] b` for every element `b` of `I`. -/
def rightDual (I : Set β) : Set α :=
  {a : α | ∀ ⦃b⦄, b ∈ I → a ~[R] b}

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