card_aut_le_card_fiber_of_connected

English

If A is connected, the size of Aut(A) does not exceed the fiber size of A.

Русский

Если A связный, размер группы автоморфизмов Aut(A) не превышает размер фибера A.

LaTeX

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

Lean4

/-- If `A` is connected, the cardinality of `Aut A` is smaller than the cardinality of the
fiber of `A`. -/
theorem card_aut_le_card_fiber_of_connected (A : C) [IsConnected A] : Nat.card (Aut A) ≤ Nat.card (F.obj A) :=
  by
  have h : Nonempty (F.obj A) := inferInstance
  obtain ⟨a⟩ := h
  apply Nat.card_le_card_of_injective
  exact evaluation_aut_injective_of_isConnected _ _ a

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