coe_sup — Mathlib

English

The underlying set of the supremum of two ideals I and J is the set of all x in P with x ≤ a ⊔ b for some a ∈ I and b ∈ J.

Русский

Основной набор верхнего предела двух идеалов I и J равен множеству всех элементов x ∈ P, для которых существует a ∈ I и b ∈ J такие, что x ≤ a ⊔ b.

LaTeX

$$$ \uparrow (I \lor J) = \{ x \in P \mid \exists a \in I, \exists b \in J, x \le a \lor b \}. $$$

Lean4

@[simp]
theorem coe_sup : ↑(s ⊔ t) = {x | ∃ a ∈ s, ∃ b ∈ t, x ≤ a ⊔ b} :=
  rfl

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