instNonemptyPullback — Mathlib

English

If E(f(x)) is nonempty for some x, then the fiber of the pullback bundle over x is nonempty.

Русский

Если существует элемент в E(f(x)) для некоторого x, то волокно вытянутого вниз биндинга над x непусто.

LaTeX

$$$$\forall {B,E,B',f,x} [\text{Nonempty}(E(f(x)))],\ \text{Nonempty}(\text{Bundle.Pullback } f E\ x).$$$$

Lean4

instance {f : B' → B} {x : B'} [Nonempty (E (f x))] : Nonempty ((f *ᵖ E) x) :=
  ‹Nonempty (E (f x))›

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