le_functorObj_iff — Mathlib

English

A formula relating V ≤ functorObj(U) to (Opens.map f).objV ≤ U for an inducing map f.

Русский

Связь между V ≤ functorObj(U) и (Opens.map f).obj V ≤ U для индукцирующего f.

LaTeX

$$$ V \le hf.functorObj(U) \iff (Opens.map f).obj V \le U.$$$

Lean4

theorem le_functorObj_iff {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f) {U : Opens X} {V : Opens Y} :
    V ≤ hf.functorObj U ↔ (Opens.map f).obj V ≤ U :=
  by
  obtain ⟨U, hU⟩ := U
  obtain ⟨t, ht, rfl⟩ := hf.isOpen_iff.mp hU
  constructor
  · exact fun i x hx ↦ (hf.mem_functorObj_iff ((Opens.map f).obj ⟨t, ht⟩)).mp (i hx)
  · intro h x hx
    refine Opens.mem_sSup.mpr ⟨⟨_, V.2.union ht⟩, Opens.ext ?_, Set.mem_union_left t hx⟩
    dsimp
    rwa [Set.union_eq_right]

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