one_le_div

Mathlib.Order.Filter.Pointwise

URI: https://scilib.ai/kg/mathlib#Filter.NeBot.one_le_div

← MathLib Explorer

English

For a nontrivial filter f, 1 ≤ f / f.

Русский

Для ненулевого фильтра f справедливо 1 ≤ f / f.

LaTeX

$$1 ≤ f / f$$

Lean4

@[to_additive]
theorem one_le_div (h : f.NeBot) : 1 ≤ f / f :=
  by
  rintro s ⟨t₁, h₁, t₂, h₂, hs⟩
  obtain ⟨a, ha₁, ha₂⟩ := Set.not_disjoint_iff.1 (h.not_disjoint h₁ h₂)
  rw [mem_one, ← div_self' a]
  exact hs (Set.div_mem_div ha₁ ha₂)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru