hasGroupoid_inf_iff — Mathlib

English

For charted spaces, HasGroupoid M (G1 ⊓ G2) if and only if HasGroupoid M G1 and HasGroupoid M G2.

Русский

Для чартизованных пространств HasGroupoid M (G1 ⊓ G2) тогда и только тогда, когда HasGroupoid M G1 и HasGroupoid M G2.

LaTeX

$$$HasGroupoid\ M\ (G_1 \sqcap G_2) \;\iff\; (HasGroupoid\ M\ G_1) \land (HasGroupoid\ M\ G_2).$$$

Lean4

theorem hasGroupoid_inf_iff {G₁ G₂ : StructureGroupoid H} :
    HasGroupoid M (G₁ ⊓ G₂) ↔ HasGroupoid M G₁ ∧ HasGroupoid M G₂ :=
  ⟨(fun h ↦ ⟨hasGroupoid_of_le h inf_le_left, hasGroupoid_of_le h inf_le_right⟩), fun ⟨h1, h2⟩ ↦
    { compatible := fun he he' ↦ ⟨h1.compatible he he', h2.compatible he he'⟩ }⟩

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