English
Under Freiman isomorphism, IsCorner is equivalent to its image under Prod.map f f, given appropriate subset relations.
Русский
При преобразовании Фримана IsCorner эквивалентно свойству образа на Prod.map f f при заданных подмножественных отношениях.
LaTeX
$$$ IsCorner (Prod.map f f '' A) (f x_1) (f y_1) (f x_2) (f y_2) \iff IsCorner A x_1 y_1 x_2 y_2 $$$
Lean4
theorem isCorner_image (hf : IsAddFreimanIso 2 s t f) (hAs : A ⊆ s ×ˢ s) (hx₁ : x₁ ∈ s) (hy₁ : y₁ ∈ s) (hx₂ : x₂ ∈ s)
(hy₂ : y₂ ∈ s) : IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂) ↔ IsCorner A x₁ y₁ x₂ y₂ :=
by
have hf' := hf.bijOn.injOn.prodMap hf.bijOn.injOn
rw [isCorner_iff, isCorner_iff]
congr!
· exact hf'.mem_image_iff hAs (mk_mem_prod hx₁ hy₁)
· exact hf'.mem_image_iff hAs (mk_mem_prod hx₁ hy₂)
· exact hf'.mem_image_iff hAs (mk_mem_prod hx₂ hy₁)
· exact hf.add_eq_add hx₁ hy₂ hx₂ hy₁
