ULift.down_inf
theorem ULift.down_inf : ∀ {α : Type u} [inst : Inf α] (a b : ULift.{u_1, u} α), (a ⊓ b).down = a.down ⊓ b.down := by
sorry
This theorem describes how the infimum operation (`inf` or `⊓`) interacts with the `ULift.down` function in Lean 4. For any type `α` equipped with an infimum operation and any two elements `a` and `b` of the type `ULift α`, the infimum of `a` and `b` after applying the `down` function is the same as the infimum of the `down` of `a` and the `down` of `b`. In other words, applying `down` before or after taking the infimum gives the same result.
More concisely: For any type `α` with an infimum operation and for all `a` and `b` in `ULift α`, `inf (down a) (down b) = down (inf a b)`.
|
ULift.down_sup
theorem ULift.down_sup : ∀ {α : Type u} [inst : Sup α] (a b : ULift.{u_1, u} α), (a ⊔ b).down = a.down ⊔ b.down := by
sorry
This theorem, `ULift.down_sup`, states that for any type `α` that has a supremum (or least upper bound), denoted as `Sup α`, and for any two `ULift` values `a` and `b` of the type `α`, the supremum of `a` and `b` when first lifted (using the `ULift` constructor) and then taken down (using the `.down` operation) is equal to the supremum of `a.down` and `b.down`. In other words, lifting does not change the order of the supremum operation.
More concisely: For any type `α` with a supremum and for all `ULift a` and `ULift b` of type `α`, `Sup (ULift.lift a) (ULift.lift b) = Sup (a.down) (b.down)`.
|