of_trivialization — Mathlib

English

If there exists a trivialization around x that contains x in its base set, then f is evenly covered at x with that fiber.

Русский

Если существует тривиализация вокруг x, содержащая x в базовом множестве, тогда f равномерно покрывает x соответствующим волокном.

LaTeX

$$$\\text{IsEvenlyCovered } f\\ x\\ I$$$

Lean4

theorem of_trivialization [DiscreteTopology I] {x : X} {t : Trivialization I f} (hx : x ∈ t.baseSet) :
    IsEvenlyCovered f x I :=
  ⟨‹_›, _, hx, t.open_baseSet, t.source_eq ▸ t.open_source,
    { toFun e := ⟨⟨f e, e.2⟩, (t e).2⟩
      invFun
        xi :=
        ⟨t.invFun (xi.1, xi.2), by rw [Set.mem_preimage, ← t.mem_source];
          exact t.map_target (t.target_eq ▸ ⟨xi.1.2, ⟨⟩⟩)⟩
      left_inv e := Subtype.ext <| t.symm_apply_mk_proj (t.mem_source.mpr e.2)
      right_inv xi := by simp [t.proj_symm_apply', t.apply_symm_apply']
      continuous_toFun :=
        (Topology.IsInducing.subtypeVal.prodMap .id).continuous_iff.mpr <|
          (continuousOn_iff_continuous_restrict.mp <| t.continuousOn_toFun.mono t.source_eq.ge).congr fun e ↦ by
            simp [t.mk_proj_snd' e.2]
      continuous_invFun :=
        Topology.IsInducing.subtypeVal.continuous_iff.mpr <|
          t.continuousOn_invFun.comp_continuous (continuous_subtype_val.prodMap continuous_id) fun ⟨x, _⟩ ↦
            t.target_eq ▸ ⟨x.2, ⟨⟩⟩ },
    fun _ ↦ by simp⟩

Похожие утверждения