isMulFreimanIso_zero_iff — Mathlib

English

Let A ⊆ α, B ⊆ β, and f: α → β. Then f is a 0-Freiman isomorphism between A and B if and only if f induces a bijection from A onto B.

Русский

Пусть A ⊆ α, B ⊆ β и f: α → β. Тогда f является нулевой Фримановой изоморфией между A и B тогда и только тогда, когда ограничение f на A образует биекцию A → B.

LaTeX

$$$IsMulFreimanIso(0,A,B,f) \\iff \\mathrm{BijOn}(f,A,B)$$$

Lean4

@[to_additive (attr := simp)]
theorem isMulFreimanIso_zero_iff : IsMulFreimanIso 0 A B f ↔ BijOn f A B :=
  ⟨fun h => h.bijOn, fun h => ⟨h, by simp_all⟩⟩

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