Mathlib.Geometry.Manifold.Instances.Real._auxLemma.2
theorem Mathlib.Geometry.Manifold.Instances.Real._auxLemma.2 : ∀ (p : Prop), (p ∨ True) = True
This theorem, `Mathlib.Geometry.Manifold.Instances.Real._auxLemma.2`, states that for any proposition `p`, the disjunction of `p` and `True` is always `True`. In other words, regardless of whether `p` is true or false, the entire expression `(p ∨ True)` will always be true, because `True` is always true by definition.
More concisely: The theorem `Mathlib.Geometry.Manifold.Instances.Real._auxLemma.2` asserts that the disjunction of any proposition `p` and `True` is always `True`.
|
Mathlib.Geometry.Manifold.Instances.Real._auxLemma.3
theorem Mathlib.Geometry.Manifold.Instances.Real._auxLemma.3 :
∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, (a ≤ max b c) = (a ≤ b ∨ a ≤ c)
This theorem states that for any linearly ordered type `α`, and for any three elements `a`, `b`, `c` of this type, `a` is less than or equal to the maximum of `b` and `c` if and only if `a` is less than or equal to `b` or `a` is less than or equal to `c`. In short, in a linear order, an element is less than or equal to the maximum of two other elements exactly when it is less than or equal to at least one of them.
More concisely: For any linearly ordered type `α` and elements `a, b, c` in `α`, `a ≤ max(b, c)` if and only if `a ≤ b` or `a ≤ c`.
|
Mathlib.Geometry.Manifold.Instances.Real._auxLemma.1
theorem Mathlib.Geometry.Manifold.Instances.Real._auxLemma.1 :
∀ {α : Type u} [inst : Preorder α] (a : α), (a ≤ a) = True
This theorem, `Mathlib.Geometry.Manifold.Instances.Real._auxLemma.1`, states that for any type `α` with a defined `Preorder` structure, any element `a` of type `α` satisfies the condition `a ≤ a`. In other words, it asserts the reflexivity property of the preorder relation, stating that for any element in a preordered set, that element is less than or equal to itself. This is always true, hence the result is `True`.
More concisely: For any type `α` with a defined preorder relation, every element `a` in `α` satisfies `a ≤ a` (reflexivity property).
|