Commit 2022-12-06 02:39 b7012a67

View on Github →

feat: port Order.Heyting.Boundary (#844) mathlib SHA: 70d50ecfd4900dd6d328da39ab7ebd516abe4025 Porting notes:

Needed to fix the proof of boundary_le_boundary_sup_sup_boundary_inf_left as simp produced a different term than in mathlib3
The scoped notation doesn't automatically introduce the notation into the current scope. ~~3. The lint error seems like a bug. Can anyone confirm?~~

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Heyting/Boundary.lean

added def Coheyting.boundary

added theorem Coheyting.boundary_bot

added theorem Coheyting.boundary_eq_bot

added theorem Coheyting.boundary_hnot_hnot

added theorem Coheyting.boundary_hnot_le

added theorem Coheyting.boundary_idem

added theorem Coheyting.boundary_inf

added theorem Coheyting.boundary_inf_le

added theorem Coheyting.boundary_le

added theorem Coheyting.boundary_le_boundary_sup_sup_boundary_inf_left

added theorem Coheyting.boundary_le_boundary_sup_sup_boundary_inf_right

added theorem Coheyting.boundary_le_hnot

added theorem Coheyting.boundary_sup_le

added theorem Coheyting.boundary_sup_sup_boundary_inf

added theorem Coheyting.boundary_top

added theorem Coheyting.hnot_boundary

added theorem Coheyting.hnot_eq_top_iff_exists_boundary

added theorem Coheyting.hnot_hnot_sup_boundary

added theorem Coheyting.inf_hnot_self