isMulFreimanHom_one_iff — Mathlib

English

Let A ⊆ α, B ⊆ β, and f: α → β. Then f is a 1-Freiman-Hom between A and B if and only if f maps A into B.

Русский

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

LaTeX

$$$IsMulFreimanHom(1,A,B,f) \\iff \\MapsTo f\\ A\\ B$$$

Lean4

@[to_additive (attr := simp) isAddFreimanHom_one_iff]
theorem isMulFreimanHom_one_iff : IsMulFreimanHom 1 A B f ↔ MapsTo f A B :=
  ⟨fun h => h.mapsTo, fun h => ⟨h, by aesop (add simp card_eq_one)⟩⟩

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