leftDual — Mathlib

English

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

Русский

LeftDual отображает произвольный набор J ⊆ α в { b ∈ β | ∀ a ∈ J, a ~R b }.

LaTeX

$$$\mathrm{leftDual}(J) = \{ b \in \beta \mid \forall a \in J,\ a \;\tilde{R}\; b \}.$$$

Lean4

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

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