subtype_val_preimage — Mathlib

English

Let G act on X and B ⊆ X be a block for this action. If C is a subaction of X with inclusion i: C → X, then the preimage of B under i, viewed as a subset of C, is also a block for the action of G.

Русский

Пусть G действует на X, B ⊆ X является блоком для этого действия. Пусть C — поддействие X с включением i: C → X. Тогда предобраз B под i, рассматриваемый как подмножество C, тоже является блоком для действия G.

LaTeX

$$$\\text{IsBlock}(G,B) \\Rightarrow \\text{IsBlock}(G,\\operatorname{Subtype.val}^{-1} B)$$$

Lean4

@[to_additive]
theorem subtype_val_preimage {C : SubMulAction G X} (hB : IsBlock G B) : IsBlock G (Subtype.val ⁻¹' B : Set C) :=
  hB.preimage C.inclusion

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