Heyting.IsRegular.eq
theorem Heyting.IsRegular.eq : ∀ {α : Type u_1} [inst : HasCompl α] {a : α}, Heyting.IsRegular a → aᶜᶜ = a
The theorem states that for any type `α` with a defined complement operation and any element `a` of type `α`, if `a` is regular in the sense of Heyting algebras (i.e., its double complement equals itself), then indeed the double complement of `a` does equal `a`. This is essentially saying that the definition of regularity for elements of a Heyting algebra holds true, namely if an element's double complement is equal to the element itself, then the double complement of the element is indeed equal to the element.
More concisely: If `α` is a type with a defined complement operation and `a` is a regular element of the Heyting algebra `α` (i.e., `a` equals its double complement), then `a` equals its double complement.
|
Heyting.Regular.coe_injective
theorem Heyting.Regular.coe_injective :
∀ {α : Type u_1} [inst : HeytingAlgebra α], Function.Injective Heyting.Regular.val
This theorem states that for any type `α` which has a Heyting Algebra structure, the function `Heyting.Regular.val` that maps each `Regular α` to `α` is injective. In other words, if we have two different elements of the set `Regular α`, their images in `α` under `Heyting.Regular.val` will also be different. This injectivity property ensures that no information is lost when we apply the `Heyting.Regular.val` function, thus it uniquely identifies each `Regular α` element by its corresponding `α` element.
More concisely: For any Heyting Algebra `α`, the function `Heyting.Regular.val` mapping `Regular α` to `α` is an injection.
|
Heyting.Regular.coe_le_coe
theorem Heyting.Regular.coe_le_coe :
∀ {α : Type u_1} [inst : HeytingAlgebra α] {a b : Heyting.Regular α}, ↑a ≤ ↑b ↔ a ≤ b
This theorem states that for any type `α` that forms a Heyting Algebra, for any two Heyting regular elements `a` and `b` of type `α`, the property that the coercion of `a` is less than or equal to the coercion of `b` is equivalent to the fact that `a` is less than or equal to `b`. Here, coercion means converting from the subtype of regular elements to the main type. This essentially says that the order relation (less than or equal to) on the subtype of regular elements corresponds to the order relation on the original type.
More concisely: For any Heyting Algebra type `α`, the relation `a ≤ b` between regular elements `a` and `b` is equivalent to the coercion `coe a ≤ coe b` on the subtype of regular elements.
|
Heyting.isRegular_of_decidable
theorem Heyting.isRegular_of_decidable : ∀ (p : Prop) [inst : Decidable p], Heyting.IsRegular p
The theorem `Heyting.isRegular_of_decidable` states that for any decidable proposition `p`, it is also Heyting-regular. In the context of Heyting algebras, a proposition is called Heyting-regular if the double negation of the proposition equals to the proposition itself. Therefore, this theorem states that for every proposition that can be decided as either true or false, the double negation of the proposition is equivalent to the proposition itself.
More concisely: In the context of Heyting algebras, a decidable proposition is equivalent to its double negation.
|