Grace/Cumulus/Real/Analysis/OpenIntervals.g17

Open in Workbench Download source

Imports

Intervals

Declarations

• openInterval def
• leftOpenInterval def
• rightOpenInterval def
• openInterval.subset_closed theorem derivation
• leftOpenInterval.subset_closed theorem derivation
• rightOpenInterval.subset_closed theorem derivation
• openInterval.subset_left_open theorem derivation
• openInterval.subset_right_open theorem derivation
• openInterval.empty_of_le theorem derivation
• openInterval.subset_reals theorem derivation
• openInterval.ball_subset theorem derivation

Source

1-- Open and half-open intervals of the real line, with their membership laws,2-- their inclusion in the closed interval with the same endpoints, and the3-- open balls inside an open interval4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Real.Analysis.OpenIntervals10import Intervals1112def openInterval (A B : Real) : Set := { X ∈ ℝ | A < X ∧ X < B }13def leftOpenInterval (A B : Real) : Set := { X ∈ ℝ | A < X ∧ X ≤ B }14def rightOpenInterval (A B : Real) : Set := { X ∈ ℝ | A ≤ X ∧ X < B }1516theorem openInterval.subset_closed (A B : Real)17  shows openInterval(A, B) ⊆ closedInterval(A, B)18proof19  intros X hX20  obtain ⟨real, lower, upper⟩ := openInterval.membership.forward with hX21  apply closedInterval.membership.backward22  exact ⟨real, ⟨realLess.implies_le with lower, realLess.implies_le with upper⟩⟩2324theorem leftOpenInterval.subset_closed (A B : Real)25  shows leftOpenInterval(A, B) ⊆ closedInterval(A, B)26proof27  intros X hX28  obtain ⟨real, lower, upper⟩ := leftOpenInterval.membership.forward with hX29  apply closedInterval.membership.backward30  exact ⟨real, ⟨realLess.implies_le with lower, upper⟩⟩3132theorem rightOpenInterval.subset_closed (A B : Real)33  shows rightOpenInterval(A, B) ⊆ closedInterval(A, B)34proof35  intros X hX36  obtain ⟨real, lower, upper⟩ := rightOpenInterval.membership.forward with hX37  apply closedInterval.membership.backward38  exact ⟨real, ⟨lower, realLess.implies_le with upper⟩⟩3940theorem openInterval.subset_left_open (A B : Real)41  shows openInterval(A, B) ⊆ leftOpenInterval(A, B)42proof43  intros X hX44  obtain ⟨real, lower, upper⟩ := openInterval.membership.forward with hX45  apply leftOpenInterval.membership.backward46  exact ⟨real, ⟨lower, realLess.implies_le with upper⟩⟩4748theorem openInterval.subset_right_open (A B : Real)49  shows openInterval(A, B) ⊆ rightOpenInterval(A, B)50proof51  intros X hX52  obtain ⟨real, lower, upper⟩ := openInterval.membership.forward with hX53  apply rightOpenInterval.membership.backward54  exact ⟨real, ⟨realLess.implies_le with lower, upper⟩⟩5556theorem openInterval.empty_of_le (A B : Real)57  requires le : B ≤ A58  shows openInterval(A, B) = ∅59proof60  ext X61  constructor62  . intro hX63    obtain ⟨real, lower, upper⟩ := openInterval.membership.forward with hX64    exfalso65    linarith66  . intro hX67    exfalso68    simpa using hX6970theorem openInterval.subset_reals (A B : Real)71  shows openInterval(A, B) ⊆ ℝ72proof73  intros X hX74  obtain ⟨real, lower, upper⟩ := openInterval.membership.forward with hX75  exact real7677-- A ball that stays between the endpoints lies in the interval.78theorem openInterval.ball_subset (A B X E : Real)79  requires lower : A ≤ X - E80  requires upper : X + E ≤ B81  shows openBall(X, E) ⊆ openInterval(A, B)82proof83  intros Y hY84  obtain ⟨realY, near⟩ := openBall.membership.forward with hY85  obtain ⟨lowerY, upperY⟩ := openBall.order_characterization.forward with hY86  apply openInterval.membership.backward87  refine ⟨realY, ?_, ?_⟩88  . linarith89  . linarith90