mem_functorObj_iff — Mathlib

English

For an inducing f, membership in the functorObj(U) corresponds to membership of f(x) in U.

Русский

Для индукционного f принадлежность x к открытой части functorObj(U) эквивалентна принадлежности f(x) U.

LaTeX

$$$ f(x) \in hf.functorObj(U) \iff x \in U. $$$

Lean4

theorem mem_functorObj_iff {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f) (U : Opens X) {x : X} :
    f x ∈ hf.functorObj U ↔ x ∈ U := by
  conv_rhs => rw [← hf.map_functorObj U]
  rfl

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