isMulFreimanIso_empty — Mathlib

English

For all f, IsMulFreimanIso n ∅ ∅ f holds; i.e., the empty domain/codomain case is always Freiman-isomorphic.

Русский

Для любого f выполняется IsMulFreimanIso n ∅ ∅ f; пустые множества образуют Фриманову изоморфию.

LaTeX

$$$IsMulFreimanIso n\\ (\\emptyset : Set α) (\\emptyset : Set β)\\ f$$$

Lean4

@[to_additive (attr := simp)]
theorem isMulFreimanIso_empty : IsMulFreimanIso n (∅ : Set α) (∅ : Set β) f
    where
  bijOn := bijOn_empty _
  map_prod_eq_map_prod s t hs ht := by simp [eq_zero_of_forall_notMem hs, eq_zero_of_forall_notMem ht]

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