Lean4
/-- If `E` is a fiber bundle over a conditionally complete linear order,
then it is trivial over any closed interval. -/
theorem exists_trivialization_Icc_subset [ConditionallyCompleteLinearOrder B] [OrderTopology B] [FiberBundle F E]
(a b : B) : ∃ e : Trivialization F (π F E), Icc a b ⊆ e.baseSet :=
by
obtain ⟨ea, hea⟩ : ∃ ea : Trivialization F (π F E), a ∈ ea.baseSet :=
⟨trivializationAt F E a, mem_baseSet_trivializationAt F E a⟩
-- If `a < b`, then `[a, b] = ∅`, and the statement is trivial
rcases lt_or_ge b a with _ | hab
·
exact
⟨ea, by simp [*]⟩
/- Let `s` be the set of points `x ∈ [a, b]` such that `E` is trivializable over `[a, x]`.
We need to show that `b ∈ s`. Let `c = Sup s`. We will show that `c ∈ s` and `c = b`. -/
set s : Set B := {x ∈ Icc a b | ∃ e : Trivialization F (π F E), Icc a x ⊆ e.baseSet}
have ha : a ∈ s := ⟨left_mem_Icc.2 hab, ea, by simp [hea]⟩
have sne : s.Nonempty := ⟨a, ha⟩
have hsb : b ∈ upperBounds s := fun x hx => hx.1.2
have sbd : BddAbove s := ⟨b, hsb⟩
set c := sSup s
have hsc : IsLUB s c := isLUB_csSup sne sbd
have hc : c ∈ Icc a b := ⟨hsc.1 ha, hsc.2 hsb⟩
obtain ⟨-, ec : Trivialization F (π F E), hec : Icc a c ⊆ ec.baseSet⟩ : c ∈ s :=
by
rcases hc.1.eq_or_lt with heq | hlt
· rwa [← heq]
refine
⟨hc, ?_⟩
/- In order to show that `c ∈ s`, consider a trivialization `ec` of `proj` over a neighborhood
of `c`. Its base set includes `(c', c]` for some `c' ∈ [a, c)`. -/
obtain ⟨ec, hc⟩ : ∃ ec : Trivialization F (π F E), c ∈ ec.baseSet :=
⟨trivializationAt F E c, mem_baseSet_trivializationAt F E c⟩
obtain ⟨c', hc', hc'e⟩ : ∃ c' ∈ Ico a c, Ioc c' c ⊆ ec.baseSet :=
(mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset hlt).1
(mem_nhdsWithin_of_mem_nhds <| IsOpen.mem_nhds ec.open_baseSet hc)
/- Since `c' < c = Sup s`, there exists `d ∈ s ∩ (c', c]`. Let `ead` be a trivialization of
`proj` over `[a, d]`. Then we can glue `ead` and `ec` into a trivialization over `[a, c]`. -/
obtain ⟨d, ⟨hdab, ead, had⟩, hd⟩ : ∃ d ∈ s, d ∈ Ioc c' c := hsc.exists_between hc'.2
refine ⟨ead.piecewiseLe ec d (had ⟨hdab.1, le_rfl⟩) (hc'e hd), subset_ite.2 ?_⟩
exact
⟨fun x hx => had ⟨hx.1.1, hx.2⟩, fun x hx => hc'e ⟨hd.1.trans (not_le.1 hx.2), hx.1.2⟩⟩
/- So, `c ∈ s`. Let `ec` be a trivialization of `proj` over `[a, c]`. If `c = b`, then we are
done. Otherwise we show that `proj` can be trivialized over a larger interval `[a, d]`,
`d ∈ (c, b]`, hence `c` is not an upper bound of `s`. -/
rcases hc.2.eq_or_lt with heq | hlt
· exact ⟨ec, heq ▸ hec⟩
rsuffices ⟨d, hdcb, hd⟩ : ∃ d ∈ Ioc c b, ∃ e : Trivialization F (π F E), Icc a d ⊆ e.baseSet
· exact ((hsc.1 ⟨⟨hc.1.trans hdcb.1.le, hdcb.2⟩, hd⟩).not_gt hdcb.1).elim
obtain ⟨d, hdcb, hd⟩ : ∃ d ∈ Ioc c b, Ico c d ⊆ ec.baseSet :=
(mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset hlt).1
(mem_nhdsWithin_of_mem_nhds <| IsOpen.mem_nhds ec.open_baseSet (hec ⟨hc.1, le_rfl⟩))
have had : Ico a d ⊆ ec.baseSet := Ico_subset_Icc_union_Ico.trans (union_subset hec hd)
by_cases he : Disjoint (Iio d) (Ioi c)
· /- If `(c, d) = ∅`, then let `ed` be a trivialization of `proj` over a neighborhood of `d`.
Then the disjoint union of `ec` restricted to `(-∞, d)` and `ed` restricted to `(c, ∞)` is
a trivialization over `[a, d]`. -/
obtain ⟨ed, hed⟩ : ∃ ed : Trivialization F (π F E), d ∈ ed.baseSet :=
⟨trivializationAt F E d, mem_baseSet_trivializationAt F E d⟩
refine
⟨d, hdcb,
(ec.restrOpen (Iio d) isOpen_Iio).disjointUnion (ed.restrOpen (Ioi c) isOpen_Ioi)
(he.mono inter_subset_right inter_subset_right),
fun x hx => ?_⟩
rcases hx.2.eq_or_lt with (rfl | hxd)
exacts [Or.inr ⟨hed, hdcb.1⟩, Or.inl ⟨had ⟨hx.1, hxd⟩, hxd⟩]
· /- If `(c, d)` is nonempty, then take `d' ∈ (c, d)`. Since the base set of `ec` includes
`[a, d)`, it includes `[a, d'] ⊆ [a, d)` as well. -/
rw [disjoint_left] at he
push_neg at he
rcases he with ⟨d', hdd' : d' < d, hd'c⟩
exact ⟨d', ⟨hd'c, hdd'.le.trans hdcb.2⟩, ec, (Icc_subset_Ico_right hdd').trans had⟩
