coe_sup_eq — Mathlib

English

Equivalent formulation: the underlying set of the join I ∨ J can be described as the set of x with x = i ⊔ j for some i ∈ I, j ∈ J (in the appropriate sense).

Русский

Эквивалентная формулировка: множество элементов объединения I ∨ J состоит из элементов вида x = i ⊔ j для некоторых i ∈ I, j ∈ J.

LaTeX

$$$ \uparrow (I \lor J) = \{ x \in P \mid \exists i \in I, \exists j \in J, x = i \lor j \}. $$$

Lean4

theorem coe_sup_eq : ↑(I ⊔ J) = {x | ∃ i ∈ I, ∃ j ∈ J, x = i ⊔ j} :=
  Set.ext fun _ ↦
    ⟨fun ⟨_, _, _, _, _⟩ ↦ eq_sup_of_le_sup ‹_› ‹_› ‹_›, fun ⟨i, _, j, _, _⟩ ↦ ⟨i, ‹_›, j, ‹_›, le_of_eq ‹_›⟩⟩

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