English
If A ⊆ s × s, then IsCornerFree A is equivalent to: for all x1,x2,y1,y2 in s, IsCorner A x1 y1 x2 y2 implies x1 = x2.
Русский
Пусть A ⊆ s × s. Тогда IsCornerFree A эквивалентно: для любых x1,x2,y1,y2 ∈ s если IsCorner A x1 y1 x2 y2, то x1 = x2.
LaTeX
$$$ IsCornerFree(A) \iff \forall x_1 \in s, \forall y_1 \in s, \forall x_2 \in s, \forall y_2 \in s, IsCorner A x_1 y_1 x_2 y_2 \Rightarrow x_1 = x_2 $$$
Lean4
/-- A convenient restatement of corner-freeness in terms of an ambient product set. -/
theorem isCornerFree_iff (hAs : A ⊆ s ×ˢ s) :
IsCornerFree A ↔
∀ ⦃x₁⦄, x₁ ∈ s → ∀ ⦃y₁⦄, y₁ ∈ s → ∀ ⦃x₂⦄, x₂ ∈ s → ∀ ⦃y₂⦄, y₂ ∈ s → IsCorner A x₁ y₁ x₂ y₂ → x₁ = x₂
where
mp hA _x₁ _ _y₁ _ _x₂ _ _y₂ _ hxy := hA hxy
mpr hA _x₁ _y₁ _x₂ _y₂
hxy := hA (hAs hxy.fst_fst_mem).1 (hAs hxy.fst_fst_mem).2 (hAs hxy.snd_fst_mem).1 (hAs hxy.fst_snd_mem).2 hxy
