comp — Mathlib

English

The composition of FreimanIso n B C g and FreimanIso n A B f is FreimanIso n A C (g ∘ f).

Русский

Композиция FreimanIso образует FreimanIso порядка n между A и C.

LaTeX

$$IsMulFreimanIso n A C (g ∘ f)$$

Lean4

@[to_additive]
theorem comp (hg : IsMulFreimanIso n B C g) (hf : IsMulFreimanIso n A B f) : IsMulFreimanIso n A C (g ∘ f)
    where
  bijOn := hg.bijOn.comp hf.bijOn
  map_prod_eq_map_prod s t hsA htA hs
    ht := by
    rw [← map_map, ← map_map]
    rw [hg.map_prod_eq_map_prod _ _ (by rwa [card_map]) (by rwa [card_map]), hf.map_prod_eq_map_prod hsA htA hs ht]
    · simpa using fun a h ↦ hf.bijOn.mapsTo (hsA h)
    · simpa using fun a h ↦ hf.bijOn.mapsTo (htA h)

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