monotone_subset — Mathlib

English

If F ⊆ G and h is an IsDynCoverOf for G, then h is also an IsDynCoverOf for F.

Русский

Если F ⊆ G и h задаёт динамическое покрытие над G, то оно является также динамическим покрытием над F.

LaTeX

$$$F \\subseteq G \\Rightarrow \\text{IsDynCoverOf } T G U n s \\Rightarrow \\text{IsDynCoverOf } T F U n s$$$

Lean4

theorem monotone_subset {T : X → X} {F G : Set X} (F_G : F ⊆ G) {U : Set (X × X)} {n : ℕ} {s : Set X}
    (h : IsDynCoverOf T G U n s) : IsDynCoverOf T F U n s :=
  F_G.trans h

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