Source indexedlemma · leanprover/lean4:v4.32.0

Set.Ico_subset_Ico_of_Icc_subset_Icc

PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:16 to 30

Mathematical statement

Exact Lean statement

lemma Set.Ico_subset_Ico_of_Icc_subset_Icc {a b c d : ℝ} (h : Set.Icc a b ⊆ Set.Icc c d) :
    Set.Ico a b ⊆ Set.Ico c d

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Set.Ico_subset_Ico_of_Icc_subset_Icc {a b c d : ℝ} (h : Set.Icc a b ⊆ Set.Icc c d) :    Set.Ico a b ⊆ Set.Ico c d := by  intro z hz  have hz' := Set.Ico_subset_Icc_self.trans h hz  have hcd : c ≤ d := by    contrapose! hz'    rw [Icc_eq_empty_of_lt hz']    exact notMem_empty _  simp only [mem_Ico, mem_Icc] at *  refine ⟨hz'.1, hz'.2.eq_or_lt.resolve_left ?_⟩  rintro rfl  apply hz.2.not_ge  have := h <| right_mem_Icc.mpr (hz.1.trans hz.2.le)  simp only [mem_Icc] at this  exact this.2