English
Let i1: U1 → V and i2: U2 → V be inclusions with V covered by U1 and U2 (V ≤ U1 ⊔ U2). If s,t ∈ F(V) satisfy F.map i1.op s = F.map i1.op t and F.map i2.op s = F.map i2.op t, then s = t.
Русский
Пусть i1: U1 → V и i2: U2 → V — вложения, покрывающие V (V ≤ U1 ⊔ U2). Если две секции s,t над V имеют одинаковые образы на U1 и на U2, то s = t.
LaTeX
$$$\forall s,t \in F(V),\ F.map i_1^{op} s = F.map i_1^{op} t \land F.map i_2^{op} s = F.map i_2^{op} t \Rightarrow s=t,$ при условии $V \le U_1 \sqcup U_2$.$$
Lean4
theorem eq_of_locally_eq₂ {U₁ U₂ V : Opens X} (i₁ : U₁ ⟶ V) (i₂ : U₂ ⟶ V) (hcover : V ≤ U₁ ⊔ U₂)
(s t : ToType (F.1.obj (op V))) (h₁ : F.1.map i₁.op s = F.1.map i₁.op t) (h₂ : F.1.map i₂.op s = F.1.map i₂.op t) :
s = t := by
classical
fapply F.eq_of_locally_eq' fun t : Bool => if t then U₁ else U₂
· exact fun i => if h : i then eqToHom (if_pos h) ≫ i₁ else eqToHom (if_neg h) ≫ i₂
· refine le_trans hcover ?_
rw [sup_le_iff]
constructor
· exact le_iSup (fun t : Bool => if t then U₁ else U₂) true
· exact le_iSup (fun t : Bool => if t then U₁ else U₂) false
· rintro ⟨_ | _⟩
any_goals exact h₁
any_goals exact h₂
