eq_sup_of_le_sup — Mathlib

English

The underlying set of I ⊔ J equals the set of all x that lie below i ⊔ j for some i ∈ I, j ∈ J.

Русский

Основной набор 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 \le i \lor j \}. $$$

Lean4

theorem eq_sup_of_le_sup {x i j : P} (hi : i ∈ I) (hj : j ∈ J) (hx : x ≤ i ⊔ j) : ∃ i' ∈ I, ∃ j' ∈ J, x = i' ⊔ j' :=
  by
  refine ⟨x ⊓ i, I.lower inf_le_right hi, x ⊓ j, J.lower inf_le_right hj, ?_⟩
  calc
    x = x ⊓ (i ⊔ j) := left_eq_inf.mpr hx
    _ = x ⊓ i ⊔ x ⊓ j := inf_sup_left _ _ _

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