English
There exists a witness c ∈ S such that a certain relation, involving the secant components of the fraction f.mk' x y, holds: ∃ c ∈ S, c · (sec_2 · x) = c · (y · sec_1).
Русский
Существует свидетелЬ c ∈ S, такой что выполняется отношение, связанное с секант-компонентами дроби f.mk' x y: ∃ c ∈ S, c·(sec_2·x) = c·(y·sec_1).
LaTeX
$$$ \exists c : S, \; \uparrow c \cdot (\uparrow(f.sec \lvert f.mk' x y).2 \cdot x) = c \cdot (y \cdot (f.sec \lvert f.mk' x y).1) $$$
Lean4
/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M`, for all `x₁ : M` and `y₁ ∈ S`,
if `x₂ : M, y₂ ∈ S` are such that `f x₁ * (f y₁)⁻¹ * f y₂ = f x₂`, then there exists `c ∈ S`
such that `x₁ * y₂ * c = x₂ * y₁ * c`. -/
@[to_additive /-- Given a Localization map `f : M →+ N` for a Submonoid `S ⊆ M`, for all `x₁ : M`
and `y₁ ∈ S`, if `x₂ : M, y₂ ∈ S` are such that `(f x₁ - f y₁) + f y₂ = f x₂`, then there exists
`c ∈ S` such that `x₁ + y₂ + c = x₂ + y₁ + c`. -/
]
theorem exists_of_sec_mk' (x) (y : S) :
∃ c : S, ↑c * (↑(f.sec <| f.mk' x y).2 * x) = c * (y * (f.sec <| f.mk' x y).1) :=
f.eq_iff_exists.1 <| f.mk'_eq_iff_eq.1 <| (mk'_sec _ _).symm
