English
Let PG1 and PG2 be pregroupoids on a space H. Suppose every property of PG1 lifts to PG2, i.e. for all f and s, PG1.property f s implies PG2.property f s. Then the groupoid of PG1 is included in the groupoid of PG2.
Русский
Пусть на пространстве H заданы прегруппоид PG1 и PG2. Пусть каждый признак PG1 распространяется на PG2, т.е. для всех f и s: PG1.property f s ⇒ PG2.property f s. Тогда группаoid PG1 содержится в PG2.groupoid.
LaTeX
$$$\\left( \\forall f,s\\, PG_1.property(f,s) \\rightarrow PG_2.property(f,s) \\right) \\rightarrow PG_1.groupoid \\le PG_2.groupoid$$
Lean4
theorem groupoid_of_pregroupoid_le (PG₁ PG₂ : Pregroupoid H) (h : ∀ f s, PG₁.property f s → PG₂.property f s) :
PG₁.groupoid ≤ PG₂.groupoid := by
refine StructureGroupoid.le_iff.2 fun e he ↦ ?_
rw [mem_groupoid_of_pregroupoid] at he ⊢
exact ⟨h _ _ he.1, h _ _ he.2⟩
