lt_card_fiber_of_mono_of_notIso — Mathlib

English

Along a mono that is not an iso, the cardinality of the fiber strictly increases.

Русский

По моно, не являющемуся изоморфизмом, кардинальность фиберы строго возрастает.

LaTeX

$$$(Mono\ f)\land \neg IsIso(f) \Rightarrow Nat.card (F.obj X) < Nat.card (F.obj Y)$$$

Lean4

/-- Along a mono that is not an iso, the cardinality of the fiber strictly increases. -/
theorem lt_card_fiber_of_mono_of_notIso {X Y : C} (f : X ⟶ Y) [Mono f] (h : ¬IsIso f) :
    Nat.card (F.obj X) < Nat.card (F.obj Y) := by
  by_contra hlt
  apply h
  apply isIso_of_mono_of_eq_card_fiber F f
  simp only [not_lt] at hlt
  exact Nat.le_antisymm (Nat.card_le_card_of_injective (F.map f) (injective_of_mono_of_preservesPullback (F.map f))) hlt

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