isDynCoverOf_empty — Mathlib

English

If F is nonempty and s is a dynamical cover of F, then s is nonempty.

Русский

Если F непусто и s является динамическим покрытием F, тогда s непусто.

LaTeX

$$$F \neq \emptyset \Rightarrow s \neq \emptyset \text{ given }IsDynCoverOf T F U n s$$$

Lean4

@[simp]
theorem isDynCoverOf_empty {T : X → X} {U : Set (X × X)} {n : ℕ} {s : Set X} : IsDynCoverOf T ∅ U n s := by
  simp only [IsDynCoverOf, empty_subset]

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