isMulFreimanIso_one_iff — Mathlib

English

If f is a 1-Freiman isomorphism between A and B, then f is bijective on A and B, and conversely.

Русский

Если f является 1‑Фримановой изоморфией между A и B, то f задаёт биективность на A и B, и наоборот.

LaTeX

$$$IsMulFreimanIso(1,A,B,f) \\iff BijOn f\\ A\\ B$$$

Lean4

@[to_additive (attr := simp) isAddFreimanIso_one_iff]
theorem isMulFreimanIso_one_iff : IsMulFreimanIso 1 A B f ↔ BijOn f A B :=
  ⟨fun h => h.bijOn, fun h => ⟨h, by aesop (add simp [card_eq_one, BijOn])⟩⟩

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