inf_erase_top — Mathlib

English

Removing the top element from a finite set does not change the infimum of the identity function: (s \\ {⊤}).inf id = s.inf id.

Русский

Удаление верхнего элемента из конечного множества не изменяет инфимума по функциям: (s \\ {⊤}).inf id = s.inf id.

LaTeX

$$$ (s\\\\.erase\\\\ top).inf id = s.inf id $$$

Lean4

@[simp]
theorem inf_erase_top [DecidableEq α] (s : Finset α) : (s.erase ⊤).inf id = s.inf id :=
  @sup_erase_bot αᵒᵈ _ _ _ _

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