closedUnderRestriction' — Mathlib

English

Restriction-closure of a structure groupoid: if G is a structure groupoid and e is in G, restricting e to an open subset s yields an element e.restr s in G.

Русский

Замыкание по ограничению: если G — Gruppoid, и e ∈ G, то ограничение e на открытое множество s принадлежит G.

LaTeX

$$$\\text{closedUnderRestriction }(G) \\Rightarrow e.restr s \\in G$ for all $e\\in G$ and IsOpen s$$

Lean4

theorem closedUnderRestriction' {G : StructureGroupoid H} [ClosedUnderRestriction G] {e : OpenPartialHomeomorph H H}
    (he : e ∈ G) {s : Set H} (hs : IsOpen s) : e.restr s ∈ G :=
  ClosedUnderRestriction.closedUnderRestriction he s hs

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