hom_infinite — Mathlib

English

If C is a component outside L and h: K ⊆ L, then the image (C.hom h) is infinite whenever C is infinite.

Русский

Если компонент вне L бесконечен, то образ через hom(h) остаётся бесконечным.

LaTeX

$$$$ (C.\text{hom }h) : \text{Set} \to \beta \quad \text{Infinite} \Rightarrow \text{Infinite}(C.\text{hom }h) $$$$

Lean4

theorem hom_infinite (C : G.ComponentCompl L) (h : K ⊆ L) (Cinf : (C : Set V).Infinite) : (C.hom h : Set V).Infinite :=
  Set.Infinite.mono (C.subset_hom h) Cinf

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