Commit 2023-01-21 18:07 a2438661

View on Github →

feat: Port/Data.Nat.Lattice (#1751)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Lattice.lean

added theorem Nat.Set.Infinite.Nat.supₛ_eq_zero

added theorem Nat.eq_Ici_of_nonempty_of_upward_closed

added theorem Nat.infᵢ_lt_succ'

added theorem Nat.infᵢ_lt_succ

added theorem Nat.infᵢ_of_empty

added theorem Nat.infₛ_add'

added theorem Nat.infₛ_add

added theorem Nat.infₛ_def

added theorem Nat.infₛ_empty

added theorem Nat.infₛ_eq_zero

added theorem Nat.infₛ_mem

added theorem Nat.infₛ_upward_closed_eq_succ_iff

added theorem Nat.nonempty_of_infₛ_eq_succ

added theorem Nat.nonempty_of_pos_infₛ

added theorem Nat.not_mem_of_lt_infₛ

added theorem Nat.supᵢ_lt_succ'

added theorem Nat.supᵢ_lt_succ

added theorem Nat.supₛ_def

added theorem Nat.supₛ_mem

added theorem Set.binterᵢ_lt_succ'

added theorem Set.binterᵢ_lt_succ

added theorem Set.bunionᵢ_lt_succ'

added theorem Set.bunionᵢ_lt_succ