overEquiv_symm_mem_over — Mathlib

English

Given X, an object Y in Over X, a sieve S on Y.left and a hypothesis that S lies in J Y.left, the symmetric image of S under the overEquiv Y belongs to the topology J over X on Y.

Русский

Пусть X — объект, Y — объект над X, S — сита на Y.left, и S ∈ J Y.left. Тогда симметрический образ S под сопоставлением overEquiv Y принадлежит топологии J над X на Y.

LaTeX

$$$\\forall X\\,\\forall Y:\\mathrm{Over}\\,X\\,\\forall S:\\mathrm{Sieve}\\,Y.left\\;\\big(S\\in J\\,Y.left\\big)\\Rightarrow (\\mathrm{Sieve}.overEquiv\\,Y)\\mathrm{symm}\\,S\\in J.over X \\ Y$$$

Lean4

theorem overEquiv_symm_mem_over {X : C} (Y : Over X) (S : Sieve Y.left) (hS : S ∈ J Y.left) :
    (Sieve.overEquiv Y).symm S ∈ (J.over X) Y := by simpa only [mem_over_iff, Equiv.apply_symm_apply] using hS

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