card_hom_le_card_fiber_of_connected

English

If A is connected, the number of morphisms A ⟶ X does not exceed the fiber size of X.

Русский

Если A связный, число морфизмов A ⟶ X не превышает размер фибера X.

LaTeX

$$$ Nat.card (A \to X) \le Nat.card (F.obj X).carrier $$$

Lean4

/-- The cardinality of morphisms `A ⟶ X` is smaller than the cardinality of
the fiber of the target if the source is connected. -/
theorem card_hom_le_card_fiber_of_connected (A X : C) [IsConnected A] : Nat.card (A ⟶ X) ≤ Nat.card (F.obj X) :=
  by
  apply Nat.card_le_card_of_injective
  exact evaluation_injective_of_isConnected F A X (Classical.arbitrary _)

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