subset_iterate_compRel — Mathlib

English

If idRel ⊆ s, then t ⊆ (s ○ ·)^[n] t for all n ∈ ℕ.

Русский

Если idRel ⊆ s, то t ⊆ (s ○ ·)^[n] t для всех n ∈ ℕ.

LaTeX

$$$\operatorname{idRel} \subseteq s \Rightarrow t \subseteq (s \circ \cdot)^{[n]} t$$$

Lean4

theorem subset_iterate_compRel {s t : Set (α × α)} (h : idRel ⊆ s) (n : ℕ) : t ⊆ (s ○ ·)^[n] t := by
  induction n generalizing t with
  | zero => exact Subset.rfl
  | succ n ihn => exact (right_subset_compRel h).trans ihn

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