lift'_neBot_iff — Mathlib

English

Assume h is monotone. Then NeBot (f.lift' h) holds if and only if for every s ∈ f, h s is nonempty.

Русский

Пусть h монотонна. Тогда NeBot (f.lift' h) эквивалентно тому, что для каждого s ∈ f множество h s непусто.

LaTeX

$$$\\mathrm{NeBot}(f.lift' h) \\iff \\forall s \\in f, (h s).Nonempty$$$

Lean4

theorem lift'_neBot_iff (hh : Monotone h) : NeBot (f.lift' h) ↔ ∀ s ∈ f, (h s).Nonempty :=
  calc
    NeBot (f.lift' h) ↔ ∀ s ∈ f, NeBot (𝓟 (h s)) := lift_neBot_iff (monotone_principal.comp hh)
    _ ↔ ∀ s ∈ f, (h s).Nonempty := by simp only [principal_neBot_iff]

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