inf_le_invariants_comp — Mathlib

English

If f,g : α → α, then any set invariant under f and g is invariant under f ∘ g.

Русский

Пусть f,g : α → α. Любое множество, инвариантное относительно f и относительно g, инвариантно и относительно композиции f ∘ g.

LaTeX

$$$Invariants(f) \\cap Invariants(g) \\le Invariants(f \\circ g)$$$

Lean4

theorem inf_le_invariants_comp (f g : α → α) : invariants f ⊓ invariants g ≤ invariants (f ∘ g) := fun s hs ↦
  ⟨hs.1.1, by rw [preimage_comp, hs.1.2, hs.2.2]⟩

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